obsolete;
authorwenzelm
Sat, 23 Feb 2019 21:32:29 +0100
changeset 69831 b35c3839d5d1
parent 69829 3bfa28b3a5b2
child 69832 b614e3e4146a
obsolete;
src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Thu Feb 21 09:15:07 2019 +0000
+++ b/src/Pure/ML/ml_process.scala	Sat Feb 23 21:32:29 2019 +0100
@@ -52,19 +52,6 @@
           fun subparagraph (_: string) = ();
           val ML_file = PolyML.use;
           """,
-          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
-            """
-              structure FixedInt = IntInf;
-              structure RunCall =
-              struct
-                open RunCall
-                val loadWord: word * word -> word =
-                  run_call2 RuntimeCalls.POLY_SYS_load_word;
-                val storeWord: word * word * word -> unit =
-                  run_call3 RuntimeCalls.POLY_SYS_assign_word;
-              end;
-            """
-          else "",
           if (Platform.is_windows)
             "fun exit 0 = OS.Process.exit OS.Process.success" +
             " | exit 1 = OS.Process.exit OS.Process.failure" +