# HG changeset patch
# User wenzelm
# Date 1535290774 -7200
# Node ID 10732941cc4be31211454f7e734528995d183715
# Parent  51fdede038c9fc99ff76f671efec386173dec563
clarified -- prefer new 'ML_export' command;

diff -r 51fdede038c9 -r 10732941cc4b src/Pure/ML_Bootstrap.thy
--- a/src/Pure/ML_Bootstrap.thy	Sat Aug 25 22:14:12 2018 +0200
+++ b/src/Pure/ML_Bootstrap.thy	Sun Aug 26 15:39:34 2018 +0200
@@ -26,16 +26,13 @@
 
 ML \<open>Proofterm.proofs := 0\<close>
 
-ML \<open>
-  Context.setmp_generic_context NONE
-    ML \<open>
-      List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
-      structure PolyML =
-      struct
-        val pointerEq = pointer_eq;
-        structure IntInf = PolyML.IntInf;
-      end;
-    \<close>
+ML_export \<open>
+  List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
+  structure PolyML =
+  struct
+    val pointerEq = pointer_eq;
+    structure IntInf = PolyML.IntInf;
+  end;
 \<close>
 
 ML \<open>\<^assert> (not (can ML \<open>open RunCall\<close>))\<close>