--- a/src/HOL/Proofs/ex/XML_Data.thy Wed Oct 02 22:01:04 2019 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy Fri Oct 04 15:30:52 2019 +0200
@@ -12,12 +12,12 @@
subsection \<open>Export and re-import of global proof terms\<close>
ML \<open>
- fun export_proof thm =
- Proofterm.encode (Thm.clean_proof_of true thm);
+ fun export_proof thy thm =
+ Proofterm.encode (Sign.consts_of thy) (Thm.clean_proof_of true thm);
fun import_proof thy xml =
let
- val prf = Proofterm.decode xml;
+ val prf = Proofterm.decode (Sign.consts_of thy) xml;
val (prf', _) = Proofterm.freeze_thaw_prf prf;
in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end;
\<close>
@@ -30,26 +30,26 @@
lemma ex: "A \<longrightarrow> A" ..
ML_val \<open>
- val xml = export_proof @{thm ex};
+ val xml = export_proof thy1 @{thm ex};
val thm = import_proof thy1 xml;
\<close>
ML_val \<open>
- val xml = export_proof @{thm de_Morgan};
+ val xml = export_proof thy1 @{thm de_Morgan};
val thm = import_proof thy1 xml;
\<close>
ML_val \<open>
- val xml = export_proof @{thm Drinker's_Principle};
+ val xml = export_proof thy1 @{thm Drinker's_Principle};
val thm = import_proof thy1 xml;
\<close>
text \<open>Some fairly large proof:\<close>
ML_val \<open>
- val xml = export_proof @{thm abs_less_iff};
+ val xml = export_proof thy1 @{thm abs_less_iff};
val thm = import_proof thy1 xml;
- \<^assert> (size (YXML.string_of_body xml) > 1000000);
+ \<^assert> (size (YXML.string_of_body xml) > 500000);
\<close>
end