author wenzelm Tue, 02 Jun 2015 10:12:29 +0200 changeset 60360 f585b1f0b4c3 parent 60359 cb8828b859a1 child 60361 88505460fde7
clarified context;
```--- 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);
*}```