diff -r 92f56fbfbab3 -r 799437173553 src/HOL/Proofs/ex/XML_Data.thy
--- 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