--- 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