--- a/src/Pure/Proof/proof_syntax.ML Tue Jul 30 19:01:51 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Jul 30 20:09:25 2019 +0200
@@ -11,7 +11,7 @@
val read_term: theory -> bool -> typ -> string -> term
val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
val proof_syntax: Proofterm.proof -> theory -> theory
- val proof_of: Proof.context -> bool -> thm -> Proofterm.proof
+ val proof_of: bool -> thm -> Proofterm.proof
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
val pretty_clean_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
@@ -177,9 +177,9 @@
(map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
end;
-fun proof_of ctxt full raw_thm =
+fun proof_of full thm =
let
- val thm = Thm.transfer' ctxt raw_thm;
+ val thy = Thm.theory_of_thm thm;
val prop = Thm.full_prop_of thm;
val prf = Thm.proof_of thm;
val prf' =
@@ -187,7 +187,7 @@
(PThm (_, ((_, prop', _, _), body)), _) =>
if prop = prop' then Proofterm.join_proof body else prf
| _ => prf)
- in if full then Proofterm.reconstruct_proof ctxt prop prf' else prf' end;
+ in if full then Proofterm.reconstruct_proof thy prop prf' else prf' end;
fun pretty_proof ctxt prf =
Proof_Context.pretty_term_abbrev
@@ -195,6 +195,6 @@
(Proofterm.term_of_proof prf);
fun pretty_clean_proof_of ctxt full thm =
- pretty_proof ctxt (Thm.clean_proof_of ctxt full thm);
+ pretty_proof ctxt (Thm.clean_proof_of full thm);
end;