# HG changeset patch
# User wenzelm
# Date 1459795599 -7200
# Node ID 82859dac5f59d785aecb4bcd8a8b44749ced3a72
# Parent  d8cf59edf819bcadb54b0df191871bcb1ff4822d
clarified bootstrap -- avoid conditional compilation in ROOT.ML;

diff -r d8cf59edf819 -r 82859dac5f59 src/Pure/ML/fixed_int_dummy.ML
--- a/src/Pure/ML/fixed_int_dummy.ML	Mon Apr 04 20:45:54 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(*  Title:      Pure/ML/fixed_int_dummy.ML
-
-FixedInt dummy that is not fixed (up to Poly/ML 5.6).
-*)
-
-structure FixedInt = IntInf;
diff -r d8cf59edf819 -r 82859dac5f59 src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Apr 04 20:45:54 2016 +0200
+++ b/src/Pure/ROOT	Mon Apr 04 20:46:39 2016 +0200
@@ -98,7 +98,6 @@
     "Isar/typedecl.ML"
     "ML/exn_debugger.ML"
     "ML/exn_properties.ML"
-    "ML/fixed_int_dummy.ML"
     "ML/ml_antiquotation.ML"
     "ML/ml_antiquotations.ML"
     "ML/ml_compiler.ML"
diff -r d8cf59edf819 -r 82859dac5f59 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Apr 04 20:45:54 2016 +0200
+++ b/src/Pure/ROOT.ML	Mon Apr 04 20:46:39 2016 +0200
@@ -8,9 +8,6 @@
 use "ML/ml_pervasive_initial.ML";
 use "ML/ml_system.ML";
 
-if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
-else use "ML/fixed_int_dummy.ML";
-
 
 (* multithreading *)
 
diff -r d8cf59edf819 -r 82859dac5f59 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Mon Apr 04 20:45:54 2016 +0200
+++ b/src/Pure/Tools/ml_process.scala	Mon Apr 04 20:46:39 2016 +0200
@@ -39,6 +39,8 @@
     val eval_init =
       if (heaps.isEmpty) {
         List(
+          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") "structure FixedInt = IntInf"
+          else "",
           if (Platform.is_windows)
             "fun exit 0 = OS.Process.exit OS.Process.success" +
             " | exit 1 = OS.Process.exit OS.Process.failure" +