--- a/src/Pure/Proof/proof_syntax.ML Tue Jul 28 21:47:03 2015 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Tue Jul 28 23:14:40 2015 +0200
@@ -14,7 +14,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: bool -> thm -> Proofterm.proof
+ val proof_of: theory -> bool -> thm -> Proofterm.proof
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
@@ -235,9 +235,9 @@
(map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
end;
-fun proof_of full thm =
+fun proof_of thy full raw_thm =
let
- val thy = Thm.theory_of_thm thm;
+ val thm = Thm.transfer thy raw_thm;
val prop = Thm.full_prop_of thm;
val prf = Thm.proof_of thm;
val prf' =
@@ -253,6 +253,6 @@
(term_of_proof prf);
fun pretty_proof_of ctxt full th =
- pretty_proof ctxt (proof_of full th);
+ pretty_proof ctxt (proof_of (Proof_Context.theory_of ctxt) full th);
end;