# HG changeset patch
# User wenzelm
# Date 1456999922 -3600
# Node ID 98fa1f9a292fe621dc6485e702327162a8be0581
# Parent  5dfcc9697f291c1865d3bd652a94b730a0350503
discontinued polyml-5.3.0;

diff -r 5dfcc9697f29 -r 98fa1f9a292f Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Wed Mar 02 19:43:31 2016 +0100
+++ b/Admin/Release/CHECKLIST	Thu Mar 03 11:12:02 2016 +0100
@@ -5,8 +5,6 @@
 
 - check Admin/components;
 
-- test polyml-5.3.0;
-
 - test 'display_drafts' command;
 
 - test "#!/usr/bin/env isabelle_scala_script";
diff -r 5dfcc9697f29 -r 98fa1f9a292f Admin/isatest/settings/at-poly
--- a/Admin/isatest/settings/at-poly	Wed Mar 02 19:43:31 2016 +0100
+++ b/Admin/isatest/settings/at-poly	Thu Mar 03 11:12:02 2016 +0100
@@ -2,11 +2,7 @@
 
 init_components /home/isabelle/contrib "$HOME/admin/components/main"
 
-  POLYML_HOME="/home/polyml/polyml-5.3.0"
-  ML_SYSTEM="polyml-5.3.0"
-  ML_PLATFORM="x86-linux"
-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 1000"
+ML_OPTIONS="-H 1000 --gcthreads 1"
 
 ISABELLE_GHC=/usr/bin/ghc
 
@@ -35,4 +31,3 @@
 ISABELLE_POLYML="$ML_HOME/poly"
 ISABELLE_SCALA="$SCALA_HOME/bin"
 ISABELLE_SMLNJ="/home/smlnj/bin/sml"
-
diff -r 5dfcc9697f29 -r 98fa1f9a292f NEWS
--- a/NEWS	Wed Mar 02 19:43:31 2016 +0100
+++ b/NEWS	Thu Mar 03 11:12:02 2016 +0100
@@ -205,7 +205,7 @@
 discontinued. INCOMPATIBILITY, use operations from the modules "XML" and
 "YXML" in Isabelle/ML or Isabelle/Scala.
 
-* SML/NJ is no longer supported.
+* SML/NJ and old versions of Poly/ML are no longer supported.
 
 
 New in Isabelle2016 (February 2016)
diff -r 5dfcc9697f29 -r 98fa1f9a292f lib/scripts/run-polyml-5.3.0
--- a/lib/scripts/run-polyml-5.3.0	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.3.0.
-
-export -n HEAP_FILE ML_TEXT TERMINATE
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-function check_file()
-{
-  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## prepare databases
-
-if [ -z "$HEAP_FILE" ]; then
-  INIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-else
-  check_file "$HEAP_FILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$HEAP_FILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $HEAP_FILE\\n\"); Posix.Process.exit 0w1));"
-fi
-
-
-## poly process
-
-ML_TEXT="$INIT $ML_TEXT"
-
-check_file "$ML_HOME/poly"
-librarypath "$ML_HOME"
-
-if [ -z "$TERMINATE" ]; then
-  FEEDER_OPTS=""
-else
-  FEEDER_OPTS="-q"
-fi
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$ML_TEXT" $FEEDER_OPTS | \
-  { read FPID; "$ML_HOME/poly" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-RC="$?"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/Concurrent/standard_thread.ML
--- a/src/Pure/Concurrent/standard_thread.ML	Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/Concurrent/standard_thread.ML	Thu Mar 03 11:12:02 2016 +0100
@@ -49,7 +49,7 @@
 type params = {name: string, stack_limit: int option, interrupts: bool};
 
 fun attributes ({stack_limit, interrupts, ...}: params) =
-  ML_Stack.limit stack_limit @
+  Thread.MaximumMLStack stack_limit ::
   (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
 
 fun fork (params: params) body =
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 03 11:12:02 2016 +0100
@@ -98,10 +98,8 @@
       | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
       | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
       | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
-      | reported loc pt =
-          (case ML_Parse_Tree.completions pt of
-            SOME names => reported_completions loc names
-          | NONE => I)
+      | reported loc (PolyML.PTcompletions names) = reported_completions loc names
+      | reported _ _ = I
     and reported_tree (loc, props) = fold (reported loc) props;
 
     val persistent_reports = reported_tree parse_tree [];
@@ -123,16 +121,14 @@
 
     fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
       | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
-      | breakpoints loc pt =
-          (case ML_Parse_Tree.breakpoint pt of
-            SOME b =>
-              let val pos = breakpoint_position loc in
-                if is_reported pos then
-                  let val id = serial ();
-                  in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
-                else I
-              end
-          | NONE => I)
+      | breakpoints loc (PolyML.PTbreakPoint b) =
+          let val pos = breakpoint_position loc in
+            if is_reported pos then
+              let val id = serial ();
+              in cons ((pos, Markup.ML_breakpoint id), (id, (b, pos))) end
+            else I
+          end
+      | breakpoints _ _ = I
     and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
 
     val all_breakpoints = rev (breakpoints_tree parse_tree []);
@@ -264,8 +260,8 @@
       PolyML.Compiler.CPFileName location_props,
       PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
-      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
-     ML_Compiler_Parameters.debug debug;
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
+      PolyML.Compiler.CPDebug debug];
 
     val _ =
       (while not (List.null (! input_buffer)) do
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ROOT_polyml-5.6.ML
--- a/src/Pure/RAW/ROOT_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(*  Title:      Pure/RAW/ROOT_polyml-5.6.ML
-    Author:     Makarius
-
-Compatibility wrapper for Poly/ML 5.6.
-*)
-
-structure Thread =
-struct
-  open Thread;
-
-  structure Thread =
-  struct
-    open Thread;
-
-    fun numProcessors () =
-      (case Thread.numPhysicalProcessors () of
-        SOME n => n
-      | NONE => Thread.numProcessors ());
-  end;
-end;
-
-use "RAW/ROOT_polyml.ML";
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 11:12:02 2016 +0100
@@ -7,10 +7,7 @@
 (* initial ML name space *)
 
 use "RAW/ml_system.ML";
-
-if ML_System.name = "polyml-5.6"
-then use "RAW/ml_name_space_polyml-5.6.ML"
-else use "RAW/ml_name_space_polyml.ML";
+use "RAW/ml_name_space.ML";
 
 if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
 else use "RAW/fixed_int_dummy.ML";
@@ -29,13 +26,6 @@
 end;
 
 
-(* ML heap operations *)
-
-if ML_System.name = "polyml-5.3.0"
-then use "RAW/ml_heap_polyml-5.3.0.ML"
-else use "RAW/ml_heap.ML";
-
-
 (* exceptions *)
 
 fun reraise exn =
@@ -46,27 +36,16 @@
 exception Interrupt = SML90.Interrupt;
 
 use "RAW/exn.ML";
-
-if ML_System.name = "polyml-5.6"
-then use "RAW/exn_trace.ML"
-else use "RAW/exn_trace_raw.ML";
+use "RAW/exn_trace.ML";
 
 
 (* multithreading *)
 
 val seconds = Time.fromReal;
 
-if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
-then ()
-else use "RAW/single_assignment_polyml.ML";
-
 open Thread;
 use "RAW/multithreading.ML";
 
-if ML_System.name = "polyml-5.6"
-then use "RAW/ml_stack_polyml-5.6.ML"
-else use "RAW/ml_stack_dummy.ML";
-
 use "RAW/unsynchronized.ML";
 val _ = PolyML.Compiler.forgetValue "ref";
 val _ = PolyML.Compiler.forgetType "ref";
@@ -93,9 +72,8 @@
 
 (* ML runtime system *)
 
-if ML_System.name = "polyml-5.6"
-then use "RAW/ml_profiling_polyml-5.6.ML"
-else use "RAW/ml_profiling_polyml.ML";
+use "RAW/ml_heap.ML";
+use "RAW/ml_profiling.ML";
 
 val pointer_eq = PolyML.pointerEq;
 
@@ -162,10 +140,6 @@
   val display_val = pretty_ml o displayVal;
 end;
 
-use "RAW/ml_compiler_parameters.ML";
-if ML_System.name = "polyml-5.6"
-then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
-
 use "RAW/ml_positions.ML";
 use "RAW/ml_compiler0.ML";
 
@@ -175,10 +149,6 @@
 PolyML.Compiler.prompt1 := "ML> ";
 PolyML.Compiler.prompt2 := "ML# ";
 
-use "RAW/ml_parse_tree.ML";
-if ML_System.name = "polyml-5.6"
-then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
-
 fun ml_make_string struct_name =
   "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
     struct_name ^ ".ML_print_depth ()))))))";
@@ -186,6 +156,4 @@
 
 (* ML debugger *)
 
-if ML_System.name = "polyml-5.6"
-then use_no_debug "RAW/ml_debugger_polyml-5.6.ML"
-else use_no_debug "RAW/ml_debugger.ML";
+use_no_debug "RAW/ml_debugger.ML";
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/exn_trace_raw.ML
--- a/src/Pure/RAW/exn_trace_raw.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-(*  Title:      Pure/RAW/exn_trace_raw.ML
-    Author:     Makarius
-
-Raw exception trace for Poly/ML 5.3.0.
-*)
-
-fun print_exception_trace (_: exn -> string) (_: string -> unit) =
-  PolyML.exception_trace;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_compiler0.ML
--- a/src/Pure/RAW/ml_compiler0.ML	Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/RAW/ml_compiler0.ML	Thu Mar 03 11:12:02 2016 +0100
@@ -58,8 +58,8 @@
       PolyML.Compiler.CPErrorMessageProc put_message,
       PolyML.Compiler.CPLineNo (fn () => ! current_line),
       PolyML.Compiler.CPFileName file,
-      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
-      ML_Compiler_Parameters.debug debug;
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false,
+      PolyML.Compiler.CPDebug debug];
     val _ =
       (while not (List.null (! in_buffer)) do
         PolyML.compiler (get, parameters) ())
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_compiler_parameters.ML
--- a/src/Pure/RAW/ml_compiler_parameters.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/RAW/ml_compiler_parameters.ML
-    Author:     Makarius
-
-Additional ML compiler parameters for Poly/ML.
-*)
-
-signature ML_COMPILER_PARAMETERS =
-sig
-  val debug: bool -> PolyML.Compiler.compilerParameters list
-end;
-
-structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
-struct
-
-fun debug _ = [];
-
-end;
\ No newline at end of file
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
--- a/src/Pure/RAW/ml_compiler_parameters_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-(*  Title:      Pure/RAW/ml_compiler_parameters_polyml-5.6.ML
-    Author:     Makarius
-
-Additional ML compiler parameters for Poly/ML 5.6, or later.
-*)
-
-structure ML_Compiler_Parameters: ML_COMPILER_PARAMETERS =
-struct
-
-fun debug b = [PolyML.Compiler.CPDebug b];
-
-end;
\ No newline at end of file
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_debugger.ML
--- a/src/Pure/RAW/ml_debugger.ML	Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/RAW/ml_debugger.ML	Thu Mar 03 11:12:02 2016 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/RAW/ml_debugger.ML
     Author:     Makarius
 
-ML debugger interface -- dummy version.
+ML debugger interface -- for Poly/ML 5.6, or later.
 *)
 
 signature ML_DEBUGGER =
@@ -10,16 +10,17 @@
   val exn_id: exn -> exn_id
   val print_exn_id: exn_id -> string
   val eq_exn_id: exn_id * exn_id -> bool
-  val on_entry: (string * 'location -> unit) option -> unit
-  val on_exit: (string * 'location -> unit) option -> unit
-  val on_exit_exception: (string * 'location -> exn -> unit) option -> unit
-  val on_breakpoint: ('location * bool Unsynchronized.ref -> unit) option -> unit
+  type location
+  val on_entry: (string * location -> unit) option -> unit
+  val on_exit: (string * location -> unit) option -> unit
+  val on_exit_exception: (string * location -> exn -> unit) option -> unit
+  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
   type state
   val state: Thread.thread -> state list
   val debug_function: state -> string
   val debug_function_arg: state -> ML_Name_Space.valueVal
   val debug_function_result: state -> ML_Name_Space.valueVal
-  val debug_location: state -> 'location
+  val debug_location: state -> location
   val debug_name_space: state -> ML_Name_Space.T
   val debug_local_name_space: state -> ML_Name_Space.T
 end;
@@ -29,36 +30,43 @@
 
 (* exceptions *)
 
-abstype exn_id = Exn_Id of string
+abstype exn_id = Exn_Id of string * int Unsynchronized.ref
 with
 
-fun exn_id exn = Exn_Id (General.exnName exn);
-fun print_exn_id (Exn_Id name) = name;
-fun eq_exn_id (Exn_Id name1, Exn_Id name2) = name1 = name2;  (*over-approximation*)
+fun exn_id exn =
+  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
+
+fun print_exn_id (Exn_Id (name, _)) = name;
+fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
 
 end;
 
+val _ =
+  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
+    let val s = print_exn_id exn_id
+    in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
+
 
 (* hooks *)
 
-fun on_entry _ = ();
-fun on_exit _ = ();
-fun on_exit_exception _ = ();
-fun on_breakpoint _ = ();
+type location = PolyML.location;
+
+val on_entry = PolyML.DebuggerInterface.setOnEntry;
+val on_exit = PolyML.DebuggerInterface.setOnExit;
+val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
+val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
 
 
-(* debugger *)
+(* debugger operations *)
 
-fun fail () = raise Fail "No debugger support on this ML platform";
-
-type state = unit;
+type state = PolyML.DebuggerInterface.debugState;
 
-fun state _ = [];
-fun debug_function () = fail ();
-fun debug_function_arg () = fail ();
-fun debug_function_result () = fail ();
-fun debug_location () = fail ();
-fun debug_name_space () = fail ();
-fun debug_local_name_space () = fail ();
+val state = PolyML.DebuggerInterface.debugState;
+val debug_function = PolyML.DebuggerInterface.debugFunction;
+val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
+val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
+val debug_location = PolyML.DebuggerInterface.debugLocation;
+val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
+val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
 
 end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_debugger_polyml-5.6.ML
--- a/src/Pure/RAW/ml_debugger_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(*  Title:      Pure/RAW/ml_debugger_polyml-5.6.ML
-    Author:     Makarius
-
-ML debugger interface -- for Poly/ML 5.6, or later.
-*)
-
-signature ML_DEBUGGER =
-sig
-  type exn_id
-  val exn_id: exn -> exn_id
-  val print_exn_id: exn_id -> string
-  val eq_exn_id: exn_id * exn_id -> bool
-  type location
-  val on_entry: (string * location -> unit) option -> unit
-  val on_exit: (string * location -> unit) option -> unit
-  val on_exit_exception: (string * location -> exn -> unit) option -> unit
-  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
-  type state
-  val state: Thread.thread -> state list
-  val debug_function: state -> string
-  val debug_function_arg: state -> ML_Name_Space.valueVal
-  val debug_function_result: state -> ML_Name_Space.valueVal
-  val debug_location: state -> location
-  val debug_name_space: state -> ML_Name_Space.T
-  val debug_local_name_space: state -> ML_Name_Space.T
-end;
-
-structure ML_Debugger: ML_DEBUGGER =
-struct
-
-(* exceptions *)
-
-abstype exn_id = Exn_Id of string * int Unsynchronized.ref
-with
-
-fun exn_id exn =
-  Exn_Id (General.exnName exn, RunCall.run_call2 RuntimeCalls.POLY_SYS_load_word (exn, 0));
-
-fun print_exn_id (Exn_Id (name, _)) = name;
-fun eq_exn_id (Exn_Id (_, id1), Exn_Id (_, id2)) = PolyML.pointerEq (id1, id2);
-
-end;
-
-val _ =
-  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
-    let val s = print_exn_id exn_id
-    in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
-
-
-(* hooks *)
-
-type location = PolyML.location;
-
-val on_entry = PolyML.DebuggerInterface.setOnEntry;
-val on_exit = PolyML.DebuggerInterface.setOnExit;
-val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
-val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
-
-
-(* debugger operations *)
-
-type state = PolyML.DebuggerInterface.debugState;
-
-val state = PolyML.DebuggerInterface.debugState;
-val debug_function = PolyML.DebuggerInterface.debugFunction;
-val debug_function_arg = PolyML.DebuggerInterface.debugFunctionArg;
-val debug_function_result = PolyML.DebuggerInterface.debugFunctionResult;
-val debug_location = PolyML.DebuggerInterface.debugLocation;
-val debug_name_space = PolyML.DebuggerInterface.debugNameSpace;
-val debug_local_name_space = PolyML.DebuggerInterface.debugLocalNameSpace;
-
-end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_heap_polyml-5.3.0.ML
--- a/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/RAW/ml_heap_polyml-5.3.0.ML
-    Author:     Makarius
-
-ML heap operations.
-*)
-
-signature ML_HEAP =
-sig
-  val share_common_data: unit -> unit
-  val save_state: string -> unit
-end;
-
-structure ML_Heap: ML_HEAP =
-struct
-  fun share_common_data () = ();
-  val save_state = PolyML.SaveState.saveState o ML_System.platform_path;
-end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_name_space.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_name_space.ML	Thu Mar 03 11:12:02 2016 +0100
@@ -0,0 +1,33 @@
+(*  Title:      Pure/RAW/ml_name_space.ML
+    Author:     Makarius
+
+Name space for Poly/ML.
+*)
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+
+  type T = PolyML.NameSpace.nameSpace;
+  val global = PolyML.globalNameSpace;
+  val forget_global_structure = PolyML.Compiler.forgetStructure;
+
+  type valueVal = Values.value;
+  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
+  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
+
+  type typeVal = TypeConstrs.typeConstr;
+  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
+
+  type fixityVal = Infixes.fixity;
+  fun displayFix (_: string, x) = Infixes.print x;
+
+  type structureVal = Structures.structureVal;
+  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
+
+  type signatureVal = Signatures.signatureVal;
+  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
+
+  type functorVal = Functors.functorVal;
+  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
+end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_name_space_polyml-5.6.ML
--- a/src/Pure/RAW/ml_name_space_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title:      Pure/RAW/ml_name_space_polyml-5.6.ML
-    Author:     Makarius
-
-Name space for Poly/ML.
-*)
-
-structure ML_Name_Space =
-struct
-  open PolyML.NameSpace;
-
-  type T = PolyML.NameSpace.nameSpace;
-  val global = PolyML.globalNameSpace;
-  val forget_global_structure = PolyML.Compiler.forgetStructure;
-
-  type valueVal = Values.value;
-  fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
-  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
-
-  type typeVal = TypeConstrs.typeConstr;
-  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
-
-  type fixityVal = Infixes.fixity;
-  fun displayFix (_: string, x) = Infixes.print x;
-
-  type structureVal = Structures.structureVal;
-  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
-
-  type signatureVal = Signatures.signatureVal;
-  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
-
-  type functorVal = Functors.functorVal;
-  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
-end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_name_space_polyml.ML
--- a/src/Pure/RAW/ml_name_space_polyml.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(*  Title:      Pure/RAW/ml_name_space_polyml.ML
-    Author:     Makarius
-
-Name space for Poly/ML.
-*)
-
-structure ML_Name_Space =
-struct
-  open PolyML.NameSpace;
-  type T = nameSpace;
-  val global = PolyML.globalNameSpace;
-  val forget_global_structure = PolyML.Compiler.forgetStructure;
-end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_parse_tree.ML
--- a/src/Pure/RAW/ml_parse_tree.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      Pure/RAW/ml_parse_tree.ML
-    Author:     Makarius
-
-Additional ML parse tree components for Poly/ML.
-*)
-
-signature ML_PARSE_TREE =
-sig
-  val completions: PolyML.ptProperties -> string list option
-  val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
-end;
-
-structure ML_Parse_Tree: ML_PARSE_TREE =
-struct
-
-fun completions _ = NONE;
-fun breakpoint _ = NONE;
-
-end;
\ No newline at end of file
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_parse_tree_polyml-5.6.ML
--- a/src/Pure/RAW/ml_parse_tree_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/RAW/ml_parse_tree_polyml-5.6.ML
-    Author:     Makarius
-
-Additional ML parse tree components for Poly/ML 5.6, or later.
-*)
-
-structure ML_Parse_Tree: ML_PARSE_TREE =
-struct
-
-fun completions (PolyML.PTcompletions x) = SOME x
-  | completions _ = NONE;
-
-fun breakpoint (PolyML.PTbreakPoint x) = SOME x
-  | breakpoint _ = NONE;
-
-end;
\ No newline at end of file
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_profiling.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_profiling.ML	Thu Mar 03 11:12:02 2016 +0100
@@ -0,0 +1,19 @@
+(*  Title:      Pure/RAW/ml_profiling.ML
+    Author:     Makarius
+
+Profiling for Poly/ML 5.6.
+*)
+
+structure ML_Profiling =
+struct
+
+fun profile_time pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
+
+fun profile_time_thread pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
+
+fun profile_allocations pr f x =
+  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
+
+end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_profiling_polyml-5.6.ML
--- a/src/Pure/RAW/ml_profiling_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      Pure/RAW/ml_profiling_polyml-5.6.ML
-    Author:     Makarius
-
-Profiling for Poly/ML 5.6.
-*)
-
-structure ML_Profiling =
-struct
-
-fun profile_time pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTime f x;
-
-fun profile_time_thread pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileTimeThisThread f x;
-
-fun profile_allocations pr f x =
-  PolyML.Profiling.profileStream pr PolyML.Profiling.ProfileAllocations f x;
-
-end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_profiling_polyml.ML
--- a/src/Pure/RAW/ml_profiling_polyml.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      Pure/RAW/ml_profiling_polyml.ML
-    Author:     Makarius
-
-Profiling for Poly/ML.
-*)
-
-structure ML_Profiling =
-struct
-
-local
-
-fun profile n f x =
-  let
-    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
-    val res = Exn.capture f x;
-    val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
-  in Exn.release res end;
-
-in
-
-fun profile_time (_: (int * string) list -> unit) f x = profile 1 f x;
-fun profile_time_thread (_: (int * string) list -> unit) f x = profile 6 f x;
-fun profile_allocations (_: (int * string) list -> unit) f x = profile 2 f x;
-
-end;
-
-end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_stack_dummy.ML
--- a/src/Pure/RAW/ml_stack_dummy.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/RAW/ml_stack_dummy.ML
-
-Maximum stack size (in words) for ML threads -- dummy version.
-*)
-
-signature ML_STACK =
-sig
-  val limit: int option -> Thread.threadAttribute list
-end;
-
-structure ML_Stack: ML_STACK =
-struct
-
-fun limit (_: int option) : Thread.threadAttribute list = [];
-
-end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/ml_stack_polyml-5.6.ML
--- a/src/Pure/RAW/ml_stack_polyml-5.6.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/RAW/ml_stack_polyml-5.6.ML
-
-Maximum stack size (in words) for ML threads -- Poly/ML 5.6, or later.
-*)
-
-signature ML_STACK =
-sig
-  val limit: int option -> Thread.threadAttribute list
-end;
-
-structure ML_Stack: ML_STACK =
-struct
-
-fun limit m = [Thread.MaximumMLStack m];
-
-end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/multithreading.ML
--- a/src/Pure/RAW/multithreading.ML	Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/RAW/multithreading.ML	Thu Mar 03 11:12:02 2016 +0100
@@ -88,8 +88,13 @@
 
 (* options *)
 
+fun num_processors () =
+  (case Thread.numPhysicalProcessors () of
+    SOME n => n
+  | NONE => Thread.numProcessors ());
+
 fun max_threads_result m =
-  if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
+  if m > 0 then m else Int.min (Int.max (num_processors (), 1), 8);
 
 val max_threads = ref 1;
 
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/RAW/single_assignment_polyml.ML
--- a/src/Pure/RAW/single_assignment_polyml.ML	Wed Mar 02 19:43:31 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(*  Title:      Pure/RAW/single_assignment_polyml.ML
-    Author:     Makarius
-
-References with single assignment.  Unsynchronized!  Emulates
-structure SingleAssignment from Poly/ML 5.4.
-*)
-
-signature SINGLE_ASSIGNMENT =
-sig
-  type 'a saref
-  exception Locked
-  val saref: unit -> 'a saref
-  val savalue: 'a saref -> 'a option
-  val saset: 'a saref * 'a -> unit
-end;
-
-structure SingleAssignment: SINGLE_ASSIGNMENT =
-struct
-
-exception Locked;
-
-abstype 'a saref = SARef of 'a option ref
-with
-
-fun saref () = SARef (ref NONE);
-
-fun savalue (SARef r) = ! r;
-
-fun saset (SARef (r as ref NONE), x) =
-      (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r)
-  | saset _ = raise Locked;
-
-end;
-
-end;
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/ROOT	Thu Mar 03 11:12:02 2016 +0100
@@ -3,65 +3,39 @@
 session RAW =
   theories
   files
-    "RAW/ROOT_polyml-5.6.ML"
     "RAW/ROOT_polyml.ML"
     "RAW/exn.ML"
     "RAW/exn_trace.ML"
-    "RAW/exn_trace_raw.ML"
     "RAW/fixed_int_dummy.ML"
     "RAW/ml_compiler0.ML"
-    "RAW/ml_compiler_parameters.ML"
-    "RAW/ml_compiler_parameters_polyml-5.6.ML"
     "RAW/ml_debugger.ML"
-    "RAW/ml_debugger_polyml-5.6.ML"
     "RAW/ml_heap.ML"
-    "RAW/ml_heap_polyml-5.3.0.ML"
-    "RAW/ml_name_space_polyml-5.6.ML"
-    "RAW/ml_name_space_polyml.ML"
-    "RAW/ml_parse_tree.ML"
-    "RAW/ml_parse_tree_polyml-5.6.ML"
+    "RAW/ml_name_space.ML"
     "RAW/ml_positions.ML"
     "RAW/ml_pretty.ML"
-    "RAW/ml_profiling_polyml-5.6.ML"
-    "RAW/ml_profiling_polyml.ML"
-    "RAW/ml_stack_dummy.ML"
-    "RAW/ml_stack_polyml-5.6.ML"
+    "RAW/ml_profiling.ML"
     "RAW/ml_system.ML"
     "RAW/multithreading.ML"
     "RAW/secure.ML"
-    "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
 
 session Pure =
   global_theories Pure
   files
-    "RAW/ROOT_polyml-5.6.ML"
     "RAW/ROOT_polyml.ML"
     "RAW/exn.ML"
     "RAW/exn_trace.ML"
-    "RAW/exn_trace_raw.ML"
     "RAW/fixed_int_dummy.ML"
     "RAW/ml_compiler0.ML"
-    "RAW/ml_compiler_parameters.ML"
-    "RAW/ml_compiler_parameters_polyml-5.6.ML"
     "RAW/ml_debugger.ML"
-    "RAW/ml_debugger_polyml-5.6.ML"
     "RAW/ml_heap.ML"
-    "RAW/ml_heap_polyml-5.3.0.ML"
-    "RAW/ml_name_space_polyml-5.6.ML"
-    "RAW/ml_name_space_polyml.ML"
-    "RAW/ml_parse_tree.ML"
-    "RAW/ml_parse_tree_polyml-5.6.ML"
+    "RAW/ml_name_space.ML"
     "RAW/ml_positions.ML"
     "RAW/ml_pretty.ML"
-    "RAW/ml_profiling_polyml-5.6.ML"
-    "RAW/ml_profiling_polyml.ML"
-    "RAW/ml_stack_dummy.ML"
-    "RAW/ml_stack_polyml-5.6.ML"
+    "RAW/ml_profiling.ML"
     "RAW/ml_system.ML"
     "RAW/multithreading.ML"
     "RAW/secure.ML"
-    "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
 
     "Concurrent/bash.ML"
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 03 11:12:02 2016 +0100
@@ -101,9 +101,7 @@
 
 use "ML/exn_properties.ML";
 
-if ML_System.name = "polyml-5.6"
-then use "ML/ml_statistics.ML"
-else use "ML/ml_statistics_dummy.ML";
+use "ML/ml_statistics.ML";
 
 use "Concurrent/standard_thread.ML";
 use "Concurrent/single_assignment.ML";
diff -r 5dfcc9697f29 -r 98fa1f9a292f src/Pure/System/system_channel.ML
--- a/src/Pure/System/system_channel.ML	Wed Mar 02 19:43:31 2016 +0100
+++ b/src/Pure/System/system_channel.ML	Thu Mar 03 11:12:02 2016 +0100
@@ -32,8 +32,7 @@
   in read [] end;
 
 fun inputN (System_Channel (in_stream, _)) n =
-  if n = 0 then ""  (*workaround for polyml-5.5.1 or earlier*)
-  else Byte.bytesToString (BinIO.inputN (in_stream, n));
+  Byte.bytesToString (BinIO.inputN (in_stream, n));
 
 fun output (System_Channel (_, out_stream)) s =
   File.output out_stream s;