src/Pure/Proof/reconstruct.ML

 
 (* cleanup for output etc. *)
 
 fun clean_proof_of ctxt full thm =
   let
-    val {prop, ...} =
+    val (_, prop) =
       Logic.unconstrainT (Thm.shyps_of thm)
         (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
   in
     Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
     |> reconstruct_proof ctxt prop