# HG changeset patch
# User wenzelm
# Date 1550953949 -3600
# Node ID b35c3839d5d1d65e0edb4f5825c5a579fac3bd64
# Parent  3bfa28b3a5b24887f68754d0c1da8f8795580b1a
obsolete;

diff -r 3bfa28b3a5b2 -r b35c3839d5d1 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" +