--- a/src/Pure/more_thm.ML Tue Jul 30 11:41:39 2019 +0200
+++ b/src/Pure/more_thm.ML Tue Jul 30 11:51:55 2019 +0200
@@ -680,8 +680,9 @@
let val thm = Thm.transfer' ctxt raw_thm
in Reconstruct.reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
-fun clean_proof_of ctxt full thm =
+fun clean_proof_of ctxt full raw_thm =
let
+ val thm = Thm.transfer' ctxt raw_thm;
val (_, prop) =
Logic.unconstrainT (Thm.shyps_of thm)
(Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
@@ -695,6 +696,7 @@
end;
+
(** forked proofs **)
structure Proofs = Theory_Data