src/Pure/more_thm.ML
changeset 70447 755d58b48cec
parent 70444 56d73e7316c4
child 70449 6e34025981be
--- a/src/Pure/more_thm.ML	Tue Jul 30 13:22:29 2019 +0200
+++ b/src/Pure/more_thm.ML	Tue Jul 30 14:35:29 2019 +0200
@@ -678,7 +678,7 @@
 
 fun reconstruct_proof_of ctxt raw_thm =
   let val thm = Thm.transfer' ctxt raw_thm
-  in Reconstruct.reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
+  in Proofterm.reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
 
 fun clean_proof_of ctxt full raw_thm =
   let
@@ -688,8 +688,8 @@
         (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
   in
     Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
-    |> Reconstruct.reconstruct_proof ctxt prop
-    |> Reconstruct.expand_proof ctxt [("", NONE)]
+    |> Proofterm.reconstruct_proof ctxt prop
+    |> Proofterm.expand_proof ctxt [("", NONE)]
     |> Proofterm.rew_proof (Proof_Context.theory_of ctxt)
     |> Proofterm.no_thm_proofs
     |> not full ? Proofterm.shrink_proof