# HG changeset patch
# User wenzelm
# Date 1535383574 -7200
# Node ID 9cfa4aa3571980facea1a36db5dd8ed912880b06
# Parent  6debac400787aa1b01b7e5a125d665e726e3a39f
tuned;

diff -r 6debac400787 -r 9cfa4aa35719 src/Pure/ML_Bootstrap.thy
--- 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