--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pervasive1.ML Wed Apr 06 11:37:37 2016 +0200
@@ -0,0 +1,17 @@
+(* Title: Pure/ML/ml_pervasive1.ML
+ Author: Makarius
+
+Pervasive ML environment: final setup.
+*)
+
+if Options.default_bool "ML_system_bootstrap" then ()
+else
+ (List.app ML_Name_Space.forget_structure
+ (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
+ ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>);
+
+structure Output: OUTPUT = Output; (*seal system channels!*)
+
+Proofterm.proofs := 0;
+
+Context.set_thread_data NONE;