# HG changeset patch # User wenzelm # Date 1459935874 -7200 # Node ID 66494de0aafe48e29c15c4739d6c6f055d3ee720 # Parent b04e9fe292239c03f1161336162d36769ab1c2d9 clarified bootstrap; diff -r b04e9fe29223 -r 66494de0aafe src/Pure/ML/ml_pervasive1.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 \structure PolyML = struct structure IntInf = PolyML.IntInf end\); -structure Output: OUTPUT = Output; (*seal system channels!*) - Proofterm.proofs := 0; Context.set_thread_data NONE; diff -r b04e9fe29223 -r 66494de0aafe src/Pure/Tools/build.ML --- 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!*)