obsolete;
authorwenzelm
Sat Feb 23 21:32:29 2019 +0100 (8 weeks ago ago)
changeset 70012b35c3839d5d1
parent 70010 3bfa28b3a5b2
child 70013 b614e3e4146a
obsolete;
src/Pure/ML/ml_process.scala
     1.1 --- a/src/Pure/ML/ml_process.scala	Thu Feb 21 09:15:07 2019 +0000
     1.2 +++ b/src/Pure/ML/ml_process.scala	Sat Feb 23 21:32:29 2019 +0100
     1.3 @@ -52,19 +52,6 @@
     1.4            fun subparagraph (_: string) = ();
     1.5            val ML_file = PolyML.use;
     1.6            """,
     1.7 -          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
     1.8 -            """
     1.9 -              structure FixedInt = IntInf;
    1.10 -              structure RunCall =
    1.11 -              struct
    1.12 -                open RunCall
    1.13 -                val loadWord: word * word -> word =
    1.14 -                  run_call2 RuntimeCalls.POLY_SYS_load_word;
    1.15 -                val storeWord: word * word * word -> unit =
    1.16 -                  run_call3 RuntimeCalls.POLY_SYS_assign_word;
    1.17 -              end;
    1.18 -            """
    1.19 -          else "",
    1.20            if (Platform.is_windows)
    1.21              "fun exit 0 = OS.Process.exit OS.Process.success" +
    1.22              " | exit 1 = OS.Process.exit OS.Process.failure" +