# HG changeset patch
# User wenzelm
# Date 1433232749 -7200
# Node ID f585b1f0b4c35b586cff8974bd9d7e05fec0fc33
# Parent  cb8828b859a15759c95bd7da3170b6e451a83dc4
clarified context;

diff -r cb8828b859a1 -r f585b1f0b4c3 src/HOL/Proofs/ex/XML_Data.thy
--- a/src/HOL/Proofs/ex/XML_Data.thy	Tue Jun 02 09:40:04 2015 +0200
+++ b/src/HOL/Proofs/ex/XML_Data.thy	Tue Jun 02 10:12:29 2015 +0200
@@ -12,9 +12,8 @@
 subsection {* Export and re-import of global proof terms *}
 
 ML {*
-  fun export_proof thm =
+  fun export_proof thy thm =
     let
-      val thy = Thm.theory_of_thm thm;
       val {prop, hyps, shyps, ...} = Thm.rep_thm thm;
       val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop));
       val prf =
@@ -40,24 +39,24 @@
 lemma ex: "A \<longrightarrow> A" ..
 
 ML_val {*
-  val xml = export_proof @{thm ex};
+  val xml = export_proof @{theory} @{thm ex};
   val thm = import_proof thy1 xml;
 *}
 
 ML_val {*
-  val xml = export_proof @{thm de_Morgan};
+  val xml = export_proof @{theory} @{thm de_Morgan};
   val thm = import_proof thy1 xml;
 *}
 
 ML_val {*
-  val xml = export_proof @{thm Drinker's_Principle};
+  val xml = export_proof @{theory} @{thm Drinker's_Principle};
   val thm = import_proof thy1 xml;
 *}
 
 text {* Some fairly large proof: *}
 
 ML_val {*
-  val xml = export_proof @{thm abs_less_iff};
+  val xml = export_proof @{theory} @{thm abs_less_iff};
   val thm = import_proof thy1 xml;
   @{assert} (size (YXML.string_of_body xml) > 1000000);
 *}