--- a/src/Pure/ML_Bootstrap.thy Mon Aug 27 15:18:18 2018 +0200
+++ b/src/Pure/ML_Bootstrap.thy Mon Aug 27 17:26:14 2018 +0200
@@ -10,9 +10,6 @@
external_file "$POLYML_EXE"
-
-subsection \<open>ML environment for virtual bootstrap\<close>
-
ML \<open>
#allStruct ML_Name_Space.global () |> List.app (fn (name, _) =>
if member (op =) ML_Name_Space.hidden_structures name then
@@ -22,14 +19,9 @@
structure Thread_Data = Thread_Data_Virtual;
structure PolyML = PolyML;
fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
-\<close>
-
-subsection \<open>Global ML environment for Isabelle/Pure\<close>
+ Proofterm.proofs := 0;
-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;
@@ -42,6 +34,7 @@
\<close>
setup \<open>Context.theory_map ML_Env.bootstrap_name_space\<close>
+
declare [[ML_read_global = false]]
end