# HG changeset patch
# User wenzelm
# Date 1456693086 -3600
# Node ID 075ef5ec115c6229b3ed01f7c8290bab4eadceb3
# Parent  9590972c2caf2fe8a91385b7891779136b8e9012# Parent  4b2018eb92e83648142eb82cb0bac12d1eb34fe9
merged

diff -r 9590972c2caf -r 075ef5ec115c Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Sun Feb 28 21:20:11 2016 +0100
+++ b/Admin/Release/CHECKLIST	Sun Feb 28 21:58:06 2016 +0100
@@ -5,7 +5,7 @@
 
 - check Admin/components;
 
-- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0;
+- test polyml-5.3.0;
 
 - test 'display_drafts' command;
 
diff -r 9590972c2caf -r 075ef5ec115c lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Sun Feb 28 21:20:11 2016 +0100
+++ b/lib/scripts/run-polyml	Sun Feb 28 21:58:06 2016 +0100
@@ -1,8 +1,9 @@
 #!/usr/bin/env bash
+# :mode=shellscript:
 #
 # Author: Makarius
 #
-# Startup script for Poly/ML 5.1 ... 5.5.
+# Startup script for Poly/ML 5.6.
 
 export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
 
@@ -39,12 +40,30 @@
 
 ## prepare databases
 
+case "$ML_PLATFORM" in
+  *-windows)
+    PLATFORM_INFILE="$(platform_path -m "$INFILE")"
+    PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
+    ;;
+  *)
+    PLATFORM_INFILE="$INFILE"
+    PLATFORM_OUTFILE="$OUTFILE"
+    ;;
+esac
+
 if [ -z "$INFILE" ]; then
   INIT=""
-  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+  case "$ML_PLATFORM" in
+    *-windows)
+      EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
+      ;;
+    *)
+      EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+      ;;
+  esac
 else
   check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
   EXIT=""
 fi
 
@@ -52,7 +71,7 @@
   MLEXIT=""
 else
   if [ -z "$INFILE" ]; then
-    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
   else
     MLEXIT="Session.save \"$OUTFILE\";"
   fi
@@ -64,16 +83,22 @@
 
 MLTEXT="$INIT $EXIT $MLTEXT"
 
-if [ -z "$TERMINATE" ]; then
-  FEEDER_OPTS=""
+if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
+  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+    --error-exit </dev/null
+  RC="$?"
 else
-  FEEDER_OPTS="-q"
+  if [ -z "$TERMINATE" ]; then
+    FEEDER_OPTS=""
+  else
+    FEEDER_OPTS="-q"
+    ML_OPTIONS="$ML_OPTIONS --error-exit"
+  fi
+  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+  RC="$?"
 fi
 
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-RC="$?"
-
 [ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 
 exit "$RC"
diff -r 9590972c2caf -r 075ef5ec115c lib/scripts/run-polyml-5.3.0
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/run-polyml-5.3.0	Sun Feb 28 21:58:06 2016 +0100
@@ -0,0 +1,81 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# Startup script for Poly/ML 5.3.0.
+
+export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
+
+
+## diagnostics
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+function fail_out()
+{
+  fail "Unable to create output heap file: \"$OUTFILE\""
+}
+
+function check_file()
+{
+  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
+}
+
+
+## compiler executables and libraries
+
+[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
+
+POLY="$ML_HOME/poly"
+check_file "$POLY"
+
+librarypath "$ML_HOME"
+
+
+
+## prepare databases
+
+if [ -z "$INFILE" ]; then
+  INIT=""
+  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
+else
+  check_file "$INFILE"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
+  EXIT=""
+fi
+
+if [ -z "$OUTFILE" ]; then
+  MLEXIT=""
+else
+  if [ -z "$INFILE" ]; then
+    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+  else
+    MLEXIT="Session.save \"$OUTFILE\";"
+  fi
+  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+fi
+
+
+## run it!
+
+MLTEXT="$INIT $EXIT $MLTEXT"
+
+if [ -z "$TERMINATE" ]; then
+  FEEDER_OPTS=""
+else
+  FEEDER_OPTS="-q"
+fi
+
+"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
+  { read FPID; "$POLY" -q $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
+RC="$?"
+
+[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
+
+exit "$RC"
+
+#:wrap=soft:maxLineLen=100:
diff -r 9590972c2caf -r 075ef5ec115c lib/scripts/run-polyml-5.5.1
--- a/lib/scripts/run-polyml-5.5.1	Sun Feb 28 21:20:11 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.5.1.
-
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-function fail_out()
-{
-  fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
-function check_file()
-{
-  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## compiler executables and libraries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-librarypath "$ML_HOME"
-
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
-  INIT=""
-  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-else
-  check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
-  EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
-  MLEXIT=""
-else
-  if [ -z "$INFILE" ]; then
-    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
-  else
-    MLEXIT="Session.save \"$OUTFILE\";"
-  fi
-  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-MLTEXT="$INIT $EXIT $MLTEXT"
-
-if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
-  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
-    --error-exit </dev/null
-  RC="$?"
-else
-  if [ -z "$TERMINATE" ]; then
-    FEEDER_OPTS=""
-  else
-    FEEDER_OPTS="-q"
-    ML_OPTIONS="$ML_OPTIONS --error-exit"
-  fi
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-  RC="$?"
-fi
-
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
diff -r 9590972c2caf -r 075ef5ec115c lib/scripts/run-polyml-5.5.2
--- a/lib/scripts/run-polyml-5.5.2	Sun Feb 28 21:20:11 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.5.2.
-
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-function fail_out()
-{
-  fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
-function check_file()
-{
-  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## compiler executables and libraries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-librarypath "$ML_HOME"
-
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
-  INIT=""
-  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-else
-  check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
-  EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
-  MLEXIT=""
-else
-  if [ -z "$INFILE" ]; then
-    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
-  else
-    MLEXIT="Session.save \"$OUTFILE\";"
-  fi
-  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-MLTEXT="$INIT $EXIT $MLTEXT"
-
-if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
-  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
-    --error-exit </dev/null
-  RC="$?"
-else
-  if [ -z "$TERMINATE" ]; then
-    FEEDER_OPTS=""
-  else
-    FEEDER_OPTS="-q"
-    ML_OPTIONS="$ML_OPTIONS --error-exit"
-  fi
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-  RC="$?"
-fi
-
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
diff -r 9590972c2caf -r 075ef5ec115c lib/scripts/run-polyml-5.6
--- a/lib/scripts/run-polyml-5.6	Sun Feb 28 21:20:11 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,106 +0,0 @@
-#!/usr/bin/env bash
-# :mode=shellscript:
-#
-# Author: Makarius
-#
-# Startup script for Poly/ML 5.6.
-
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-function fail_out()
-{
-  fail "Unable to create output heap file: \"$OUTFILE\""
-}
-
-function check_file()
-{
-  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-
-## compiler executables and libraries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-librarypath "$ML_HOME"
-
-
-
-## prepare databases
-
-case "$ML_PLATFORM" in
-  *-windows)
-    PLATFORM_INFILE="$(platform_path -m "$INFILE")"
-    PLATFORM_OUTFILE="$(platform_path -m "$OUTFILE")"
-    ;;
-  *)
-    PLATFORM_INFILE="$INFILE"
-    PLATFORM_OUTFILE="$OUTFILE"
-    ;;
-esac
-
-if [ -z "$INFILE" ]; then
-  INIT=""
-  case "$ML_PLATFORM" in
-    *-windows)
-      EXIT="fun exit 0 = OS.Process.exit OS.Process.success | exit 1 = OS.Process.exit OS.Process.failure | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc));"
-      ;;
-    *)
-      EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-      ;;
-  esac
-else
-  check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
-  EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
-  MLEXIT=""
-else
-  if [ -z "$INFILE" ]; then
-    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$PLATFORM_OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); OS.Process.exit OS.Process.success);"
-  else
-    MLEXIT="Session.save \"$OUTFILE\";"
-  fi
-  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-MLTEXT="$INIT $EXIT $MLTEXT"
-
-if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
-  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
-    --error-exit </dev/null
-  RC="$?"
-else
-  if [ -z "$TERMINATE" ]; then
-    FEEDER_OPTS=""
-  else
-    FEEDER_OPTS="-q"
-    ML_OPTIONS="$ML_OPTIONS --error-exit"
-  fi
-  "$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-    { read FPID; "$POLY" -q -i $ML_OPTIONS; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-  RC="$?"
-fi
-
-[ -n "$OUTFILE" -a -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-
-exit "$RC"
-
-#:wrap=soft:maxLineLen=100:
diff -r 9590972c2caf -r 075ef5ec115c src/Pure/ML/ml_statistics.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_statistics.ML	Sun Feb 28 21:58:06 2016 +0100
@@ -0,0 +1,59 @@
+(*  Title:      Pure/ML/ml_statistics.ML
+    Author:     Makarius
+
+ML runtime statistics for Poly/ML 5.5.0 or later.
+*)
+
+signature ML_STATISTICS =
+sig
+  val get: unit -> Properties.T
+end;
+
+structure ML_Statistics: ML_STATISTICS =
+struct
+
+fun get () =
+  let
+    val
+     {gcFullGCs,
+      gcPartialGCs,
+      sizeAllocation,
+      sizeAllocationFree,
+      sizeHeap,
+      sizeHeapFreeLastFullGC,
+      sizeHeapFreeLastGC,
+      threadsInML,
+      threadsTotal,
+      threadsWaitCondVar,
+      threadsWaitIO,
+      threadsWaitMutex,
+      threadsWaitSignal,
+      timeGCSystem,
+      timeGCUser,
+      timeNonGCSystem,
+      timeNonGCUser,
+      userCounters} = PolyML.Statistics.getLocalStats ();
+    val user_counters =
+      Vector.foldri
+        (fn (i, j, res) => ("user_counter" ^ Markup.print_int i, Markup.print_int j) :: res)
+        [] userCounters;
+  in
+    [("full_GCs", Markup.print_int gcFullGCs),
+     ("partial_GCs", Markup.print_int gcPartialGCs),
+     ("size_allocation", Markup.print_int sizeAllocation),
+     ("size_allocation_free", Markup.print_int sizeAllocationFree),
+     ("size_heap", Markup.print_int sizeHeap),
+     ("size_heap_free_last_full_GC", Markup.print_int sizeHeapFreeLastFullGC),
+     ("size_heap_free_last_GC", Markup.print_int sizeHeapFreeLastGC),
+     ("threads_in_ML", Markup.print_int threadsInML),
+     ("threads_total", Markup.print_int threadsTotal),
+     ("threads_wait_condvar", Markup.print_int threadsWaitCondVar),
+     ("threads_wait_IO", Markup.print_int threadsWaitIO),
+     ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
+     ("threads_wait_signal", Markup.print_int threadsWaitSignal),
+     ("time_CPU", Markup.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
+     ("time_GC", Markup.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
+    user_counters
+  end;
+
+end;
diff -r 9590972c2caf -r 075ef5ec115c src/Pure/ML/ml_statistics_polyml-5.5.0.ML
--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Sun Feb 28 21:20:11 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      Pure/ML/ml_statistics_polyml-5.5.0.ML
-    Author:     Makarius
-
-ML runtime statistics for Poly/ML 5.5.0.
-*)
-
-signature ML_STATISTICS =
-sig
-  val get: unit -> Properties.T
-end;
-
-structure ML_Statistics: ML_STATISTICS =
-struct
-
-fun get () =
-  let
-    val
-     {gcFullGCs,
-      gcPartialGCs,
-      sizeAllocation,
-      sizeAllocationFree,
-      sizeHeap,
-      sizeHeapFreeLastFullGC,
-      sizeHeapFreeLastGC,
-      threadsInML,
-      threadsTotal,
-      threadsWaitCondVar,
-      threadsWaitIO,
-      threadsWaitMutex,
-      threadsWaitSignal,
-      timeGCSystem,
-      timeGCUser,
-      timeNonGCSystem,
-      timeNonGCUser,
-      userCounters} = PolyML.Statistics.getLocalStats ();
-    val user_counters =
-      Vector.foldri
-        (fn (i, j, res) => ("user_counter" ^ Markup.print_int i, Markup.print_int j) :: res)
-        [] userCounters;
-  in
-    [("full_GCs", Markup.print_int gcFullGCs),
-     ("partial_GCs", Markup.print_int gcPartialGCs),
-     ("size_allocation", Markup.print_int sizeAllocation),
-     ("size_allocation_free", Markup.print_int sizeAllocationFree),
-     ("size_heap", Markup.print_int sizeHeap),
-     ("size_heap_free_last_full_GC", Markup.print_int sizeHeapFreeLastFullGC),
-     ("size_heap_free_last_GC", Markup.print_int sizeHeapFreeLastGC),
-     ("threads_in_ML", Markup.print_int threadsInML),
-     ("threads_total", Markup.print_int threadsTotal),
-     ("threads_wait_condvar", Markup.print_int threadsWaitCondVar),
-     ("threads_wait_IO", Markup.print_int threadsWaitIO),
-     ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
-     ("threads_wait_signal", Markup.print_int threadsWaitSignal),
-     ("time_CPU", Markup.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
-     ("time_GC", Markup.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
-    user_counters
-  end;
-
-end;
-
diff -r 9590972c2caf -r 075ef5ec115c src/Pure/RAW/ROOT_polyml-5.5.2.ML
--- a/src/Pure/RAW/ROOT_polyml-5.5.2.ML	Sun Feb 28 21:20:11 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  Title:      Pure/RAW/ROOT_polyml-5.5.2.ML
-    Author:     Makarius
-
-Compatibility wrapper for Poly/ML 5.5.2.
-*)
-
-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 9590972c2caf -r 075ef5ec115c src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Sun Feb 28 21:20:11 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Sun Feb 28 21:58:06 2016 +0100
@@ -59,13 +59,9 @@
 
 use "RAW/exn.ML";
 
-fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
-
-if ML_System.name = "polyml-5.5.1"
-  orelse ML_System.name = "polyml-5.5.2"
-  orelse ML_System.name = "polyml-5.6"
-then use "RAW/exn_trace_polyml-5.5.1.ML"
-else ();
+if ML_System.name = "polyml-5.6"
+then use "RAW/exn_trace.ML"
+else use "RAW/exn_trace_raw.ML";
 
 
 (* multithreading *)
diff -r 9590972c2caf -r 075ef5ec115c src/Pure/RAW/exn_trace.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/exn_trace.ML	Sun Feb 28 21:58:06 2016 +0100
@@ -0,0 +1,15 @@
+(*  Title:      Pure/RAW/exn_trace.ML
+    Author:     Makarius
+
+Exception trace via ML output, for Poly/ML 5.5.1 or later.
+*)
+
+fun print_exception_trace exn_message output e =
+  PolyML.Exception.traceException
+    (e, fn (trace, exn) =>
+      let
+        val title = "Exception trace - " ^ exn_message exn;
+        val _ = output (String.concatWith "\n" (title :: trace));
+      in reraise exn end);
+
+PolyML.Compiler.reportExhaustiveHandlers := true;
diff -r 9590972c2caf -r 075ef5ec115c src/Pure/RAW/exn_trace_polyml-5.5.1.ML
--- a/src/Pure/RAW/exn_trace_polyml-5.5.1.ML	Sun Feb 28 21:20:11 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/RAW/exn_trace_polyml-5.5.1.ML
-    Author:     Makarius
-
-Exception trace for Poly/ML 5.5.1 via ML output.
-*)
-
-fun print_exception_trace exn_message output e =
-  PolyML.Exception.traceException
-    (e, fn (trace, exn) =>
-      let
-        val title = "Exception trace - " ^ exn_message exn;
-        val _ = output (String.concatWith "\n" (title :: trace));
-      in reraise exn end);
-
-PolyML.Compiler.reportExhaustiveHandlers := true;
-
diff -r 9590972c2caf -r 075ef5ec115c src/Pure/RAW/exn_trace_raw.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/exn_trace_raw.ML	Sun Feb 28 21:58:06 2016 +0100
@@ -0,0 +1,8 @@
+(*  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 9590972c2caf -r 075ef5ec115c src/Pure/ROOT
--- a/src/Pure/ROOT	Sun Feb 28 21:20:11 2016 +0100
+++ b/src/Pure/ROOT	Sun Feb 28 21:58:06 2016 +0100
@@ -3,12 +3,12 @@
 session RAW =
   theories
   files
-    "RAW/ROOT_polyml-5.5.2.ML"
     "RAW/ROOT_polyml-5.6.ML"
     "RAW/ROOT_polyml.ML"
     "RAW/compiler_polyml.ML"
     "RAW/exn.ML"
-    "RAW/exn_trace_polyml-5.5.1.ML"
+    "RAW/exn_trace.ML"
+    "RAW/exn_trace_raw.ML"
     "RAW/fixed_int_dummy.ML"
     "RAW/ml_compiler_parameters.ML"
     "RAW/ml_compiler_parameters_polyml-5.6.ML"
@@ -35,12 +35,12 @@
 session Pure =
   global_theories Pure
   files
-    "RAW/ROOT_polyml-5.5.2.ML"
     "RAW/ROOT_polyml-5.6.ML"
     "RAW/ROOT_polyml.ML"
     "RAW/compiler_polyml.ML"
     "RAW/exn.ML"
-    "RAW/exn_trace_polyml-5.5.1.ML"
+    "RAW/exn_trace.ML"
+    "RAW/exn_trace_raw.ML"
     "RAW/fixed_int_dummy.ML"
     "RAW/ml_compiler_parameters.ML"
     "RAW/ml_compiler_parameters_polyml-5.6.ML"
@@ -169,8 +169,8 @@
     "ML/ml_lex.ML"
     "ML/ml_options.ML"
     "ML/ml_parse.ML"
+    "ML/ml_statistics.ML"
     "ML/ml_statistics_dummy.ML"
-    "ML/ml_statistics_polyml-5.5.0.ML"
     "ML/ml_syntax.ML"
     "PIDE/active.ML"
     "PIDE/command.ML"
diff -r 9590972c2caf -r 075ef5ec115c src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Feb 28 21:20:11 2016 +0100
+++ b/src/Pure/ROOT.ML	Sun Feb 28 21:58:06 2016 +0100
@@ -96,11 +96,8 @@
 
 use "ML/exn_properties.ML";
 
-if ML_System.name = "polyml-5.5.0"
-  orelse ML_System.name = "polyml-5.5.1"
-  orelse ML_System.name = "polyml-5.5.2"
-  orelse ML_System.name = "polyml-5.6"
-then use "ML/ml_statistics_polyml-5.5.0.ML"
+if ML_System.name = "polyml-5.6"
+then use "ML/ml_statistics.ML"
 else use "ML/ml_statistics_dummy.ML";
 
 use "Concurrent/standard_thread.ML";