--- a/src/Pure/ML_Bootstrap.thy Sun Apr 10 21:30:48 2016 +0200
+++ b/src/Pure/ML_Bootstrap.thy Sun Apr 10 21:46:12 2016 +0200
@@ -8,13 +8,33 @@
imports Pure
begin
+subsection \<open>Standard ML environment for virtual bootstrap\<close>
+
setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
SML_import \<open>
-structure Output_Primitives = Output_Primitives_Virtual;
-structure Thread_Data = Thread_Data_Virtual;
+ structure Output_Primitives = Output_Primitives_Virtual;
+ structure Thread_Data = Thread_Data_Virtual;
\<close>
+
+subsection \<open>Final setup of global ML environment\<close>
+
+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 structure IntInf = PolyML.IntInf end;
+ \<close>
+\<close>
+
+ML \<open>@{assert} (not (can ML \<open>open RunCall\<close>))\<close>
+
+
+subsection \<open>Switch to bootstrap environment\<close>
+
setup \<open>Config.put_global ML_Env.SML_environment true\<close>
end