--- 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;
--- 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"
--- 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 *)
--- 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" +