clarified bootstrap;
authorwenzelm
Wed, 06 Apr 2016 11:44:34 +0200
changeset 62884 66494de0aafe
parent 62883 b04e9fe29223
child 62885 108630498c00
clarified bootstrap;
src/Pure/ML/ml_pervasive1.ML
src/Pure/Tools/build.ML
--- a/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 11:37:37 2016 +0200
+++ b/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 11:44:34 2016 +0200
@@ -10,8 +10,6 @@
     (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;
--- a/src/Pure/Tools/build.ML	Wed Apr 06 11:37:37 2016 +0200
+++ b/src/Pure/Tools/build.ML	Wed Apr 06 11:44:34 2016 +0200
@@ -193,3 +193,5 @@
     in Output.protocol_message (Markup.build_theories_result id) [result] end);
 
 end;
+
+structure Output: OUTPUT = Output;  (*seal system channels!*)