# HG changeset patch
# User wenzelm
# Date 1455748175 -3600
# Node ID ab76bd43c14a764d0037ba1316bffcdc249298da
# Parent  7f927120b5a2f11fe728125e87e5a8cec4180216# Parent  e307a410f46c66ac9261cbf4f2211c80f4fc469a
merged

diff -r 7f927120b5a2 -r ab76bd43c14a Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Wed Feb 17 21:51:58 2016 +0100
+++ b/Admin/Release/CHECKLIST	Wed Feb 17 23:29:35 2016 +0100
@@ -1,11 +1,11 @@
 Checklist for official releases
 ===============================
 
-- check latest updates of polyml, smlnj, jdk, scala, jedit;
+- check latest updates of polyml, jdk, scala, jedit;
 
 - check Admin/components;
 
-- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
+- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0;
 
 - test 'display_drafts' command;
 
diff -r 7f927120b5a2 -r ab76bd43c14a Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Wed Feb 17 21:51:58 2016 +0100
+++ b/Admin/isatest/isatest-makeall	Wed Feb 17 23:29:35 2016 +0100
@@ -24,7 +24,7 @@
   echo "  Leaves messages in ${ERRORLOG} and ${LOGPREFIX} if it fails."
   echo
   echo "Examples:"
-  echo "  $PRG ~/settings/at-poly ~/settings/at-sml"
+  echo "  $PRG ~/settings/at-poly"
   echo "  $PRG -l \"HOL-Library HOL-Bali\" ~/settings/at-poly"
   exit 1
 }
@@ -92,14 +92,7 @@
 
     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
 
-    case "$SETTINGS" in
-      *sml*)
-        BUILD_ARGS="-o timeout=72000 $BUILD_ARGS"
-        ;;
-      *)
-        BUILD_ARGS="-o timeout=10800 $BUILD_ARGS"
-        ;;
-    esac
+    BUILD_ARGS="-o timeout=10800 $BUILD_ARGS"
 
     # logfile setup
 
diff -r 7f927120b5a2 -r ab76bd43c14a Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Wed Feb 17 21:51:58 2016 +0100
+++ b/Admin/isatest/isatest-makedist	Wed Feb 17 23:29:35 2016 +0100
@@ -102,8 +102,6 @@
 
 $SSH lxbroy10 "$MAKEALL -x HOL-Proofs $HOME/settings/at64-poly"
 sleep 15
-$SSH lxbroy3 "$MAKEALL -l HOL-Unix $HOME/settings/at-sml-dev-e"
-sleep 15
 $SSH lxbroy4 "
   $MAKEALL -l HOL-Library $HOME/settings/at-poly;
   $MAKEALL -l HOL-Library $HOME/settings/at-poly-e;
diff -r 7f927120b5a2 -r ab76bd43c14a Admin/isatest/isatest-stats
--- a/Admin/isatest/isatest-stats	Wed Feb 17 21:51:58 2016 +0100
+++ b/Admin/isatest/isatest-stats	Wed Feb 17 23:29:35 2016 +0100
@@ -6,7 +6,7 @@
 
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
-PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly-M8-skip_proofs mac-poly64-M8 at-sml-dev"
+PLATFORMS="at-poly at-poly-test afp at64-poly mac-poly-M2 mac-poly-M4 mac-poly64-M2 mac-poly64-M4 mac-poly-M8 mac-poly-M8-skip_proofs mac-poly64-M8"
 
 ISABELLE_SESSIONS="
   HOL
diff -r 7f927120b5a2 -r ab76bd43c14a Admin/isatest/settings/at-sml-dev-e
--- a/Admin/isatest/settings/at-sml-dev-e	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-
-ML_SYSTEM=smlnj
-ML_HOME="/home/smlnj/110.79/bin"
-ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
-ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-
-ISABELLE_GHC=/usr/bin/ghc
-
-ISABELLE_HOME_USER="$HOME/isabelle-at-sml-dev-e"
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf"
-
diff -r 7f927120b5a2 -r ab76bd43c14a NEWS
--- a/NEWS	Wed Feb 17 21:51:58 2016 +0100
+++ b/NEWS	Wed Feb 17 23:29:35 2016 +0100
@@ -136,6 +136,12 @@
 INCOMPATIBILITY.
 
 
+*** System ***
+
+* SML/NJ is no longer supported.
+
+
+
 New in Isabelle2016 (February 2016)
 -----------------------------------
 
diff -r 7f927120b5a2 -r ab76bd43c14a etc/settings
--- a/etc/settings	Wed Feb 17 21:51:58 2016 +0100
+++ b/etc/settings	Wed Feb 17 23:29:35 2016 +0100
@@ -129,17 +129,9 @@
 
 
 ###
-### Misc old-style settings
+### Misc settings
 ###
 
-# Standard ML of New Jersey (slow!)
-#ML_SYSTEM=smlnj-110
-#ML_HOME="/usr/local/smlnj/bin"
-#ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
-#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-#SMLNJ_CYGWIN_RUNTIME=1
-
-# Misc programming languages
 #ISABELLE_GHC="/usr/bin/ghc"
 #ISABELLE_OCAML="/usr/bin/ocaml"
 #ISABELLE_SWIPL="/usr/bin/swipl"
diff -r 7f927120b5a2 -r ab76bd43c14a lib/scripts/getsettings
--- a/lib/scripts/getsettings	Wed Feb 17 21:51:58 2016 +0100
+++ b/lib/scripts/getsettings	Wed Feb 17 23:29:35 2016 +0100
@@ -290,16 +290,6 @@
 #enforce JAVA_HOME
 export JAVA_HOME="$ISABELLE_JDK_HOME/jre"
 
-#build condition etc.
-case "$ML_SYSTEM" in
-  polyml*)
-    ML_SYSTEM_POLYML="true"
-    ;;
-  *)
-    ML_SYSTEM_POLYML=""
-    ;;
-esac
-
 set +o allexport
 
 fi
diff -r 7f927120b5a2 -r ab76bd43c14a lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Markus Wenzel, TU Muenchen
-#
-# SML/NJ startup script (for 110 or later).
-
-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_mlhome_file()
-{
-  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
-}
-
-function check_heap_file()
-{
-  if [ ! -f "$1" ]; then
-    echo "Expected to find ML heap file $1" >&2
-    return 1
-  else
-    return 0
-  fi
-}
-
-
-
-## compiler binaries
-
-[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
-
-SML="$ML_HOME/sml"
-ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"
-
-check_mlhome_file "$SML"
-check_mlhome_file "$ARCH_N_OPSYS"
-
-eval $("$ARCH_N_OPSYS")
-
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
-  EXIT="fun exit rc = Posix.Process.exit (Word8.fromInt rc);"
-  DB=""
-else
-  EXIT=""
-  DB="@SMLload=$INFILE"
-fi
-
-if [ -z "$OUTFILE" ]; then
-  MLEXIT=""
-else
-  if [ -z "$INFILE" ]; then
-    MLEXIT="if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};"
-  else
-    MLEXIT="Session.save \"$OUTFILE\";"
-  fi
-  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-fi
-
-
-## run it!
-
-MLTEXT="$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; "$SML" $ML_OPTIONS "$DB"; RC="$?"; kill -TERM "$FPID"; exit "$RC"; }
-RC="$?"
-
-
-## fix heap file name and permissions
-
-if [ -n "$OUTFILE" ]; then
-  check_heap_file "$OUTFILE" && [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-fi
-
-exit "$RC"
diff -r 7f927120b5a2 -r ab76bd43c14a src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Doc/Implementation/ML.thy	Wed Feb 17 23:29:35 2016 +0100
@@ -505,7 +505,7 @@
   ML and Isar are intertwined via an open-ended bootstrap process that
   provides more and more programming facilities and logical content in an
   alternating manner. Bootstrapping starts from the raw environment of
-  existing implementations of Standard ML (mainly Poly/ML, but also SML/NJ).
+  existing implementations of Standard ML (mainly Poly/ML).
 
   Isabelle/Pure marks the point where the raw ML toplevel is superseded by
   Isabelle/ML within the Isar theory and proof language, with a uniform
@@ -1379,8 +1379,7 @@
   \<^descr> Type @{ML_type int} represents regular mathematical integers, which are
   \<^emph>\<open>unbounded\<close>. Overflow is treated properly, but should never happen in
   practice.\<^footnote>\<open>The size limit for integer bit patterns in memory is 64\,MB for
-  32-bit Poly/ML, and much higher for 64-bit systems.\<close> This works uniformly
-  for all supported ML platforms (Poly/ML and SML/NJ).
+  32-bit Poly/ML, and much higher for 64-bit systems.\<close>
 
   Literal integers in ML text are forced to be of this one true integer type
   --- adhoc overloading of SML97 is disabled.
diff -r 7f927120b5a2 -r ab76bd43c14a src/Doc/ROOT
--- a/src/Doc/ROOT	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Doc/ROOT	Wed Feb 17 23:29:35 2016 +0100
@@ -126,7 +126,7 @@
     "root.tex"
 
 session Implementation (doc) in "Implementation" = "HOL-Proofs" +
-  options [condition = ML_SYSTEM_POLYML, document_variants = "implementation", quick_and_dirty]
+  options [document_variants = "implementation", quick_and_dirty]
   theories
     Eq
     Integration
diff -r 7f927120b5a2 -r ab76bd43c14a src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Doc/System/Basics.thy	Wed Feb 17 23:29:35 2016 +0100
@@ -187,12 +187,6 @@
   of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
   values.
 
-  \<^descr>[@{setting_def ML_SYSTEM_POLYML}\<open>\<^sup>*\<close>] is \<^verbatim>\<open>true\<close> for @{setting ML_SYSTEM}
-  values derived from Poly/ML, as opposed to SML/NJ where it is empty. This is
-  particularly useful with the build option @{system_option condition}
-  (\secref{sec:system-options}) to restrict big sessions to something that
-  SML/NJ can still handle.
-
   \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
   Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
   essential for Isabelle/Scala and other JVM-based tools to work properly.
diff -r 7f927120b5a2 -r ab76bd43c14a src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/HOL/ROOT	Wed Feb 17 23:29:35 2016 +0100
@@ -18,7 +18,7 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty = false]
+  options [document = false, quick_and_dirty = false]
   theories Proofs (*sequential change of global flag!*)
   theories "~~/src/HOL/Library/Old_Datatype"
   files
@@ -246,24 +246,24 @@
   document_files "root.bib" "root.tex"
 
 session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
-  options [condition = ML_SYSTEM_POLYML, document = false, browser_info = false]
+  options [document = false, browser_info = false]
   theories
     Generate
     Generate_Binary_Nat
     Generate_Target_Nat
     Generate_Efficient_Datastructures
     Generate_Pretty_Char
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_GHC"]
+  theories [condition = "ISABELLE_GHC"]
     Code_Test_GHC
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_MLTON"]
+  theories [condition = "ISABELLE_MLTON"]
     Code_Test_MLton
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_OCAMLC"]
+  theories [condition = "ISABELLE_OCAMLC"]
     Code_Test_OCaml
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_POLYML"]
+  theories [condition = "ISABELLE_POLYML"]
     Code_Test_PolyML
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SCALA"]
+  theories [condition = "ISABELLE_SCALA"]
     Code_Test_Scala
-  theories [condition = "ML_SYSTEM_POLYML,ISABELLE_SMLNJ"]
+  theories [condition = "ISABELLE_SMLNJ"]
     Code_Test_SMLNJ
 
 session "HOL-Metis_Examples" in Metis_Examples = HOL +
@@ -395,11 +395,11 @@
   description {*
     Various decision procedures, typically involving reflection.
   *}
-  options [condition = ML_SYSTEM_POLYML, document = false]
+  options [document = false]
   theories Decision_Procs
 
 session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
-  options [condition = ML_SYSTEM_POLYML, document = false, parallel_proofs = 0]
+  options [document = false, parallel_proofs = 0]
   theories
     Hilbert_Classical
     XML_Data
@@ -408,7 +408,7 @@
   description {*
     Examples for program extraction in Higher-Order Logic.
   *}
-  options [condition = ML_SYSTEM_POLYML, parallel_proofs = 0, quick_and_dirty = false]
+  options [parallel_proofs = 0, quick_and_dirty = false]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Numeral"
     "~~/src/HOL/Library/Monad_Syntax"
@@ -433,7 +433,7 @@
     The paper "More Church-Rosser Proofs (in Isabelle/HOL)" describes the whole
     theory (see http://www.in.tum.de/~nipkow/pubs/jar2001.html).
   *}
-  options [condition = ML_SYSTEM_POLYML, print_mode = "no_brackets",
+  options [print_mode = "no_brackets",
     parallel_proofs = 0, quick_and_dirty = false]
   theories [document = false]
     "~~/src/HOL/Library/Code_Target_Int"
@@ -532,7 +532,6 @@
   description {*
     Miscellaneous examples for Higher-Order Logic.
   *}
-  options [condition = ML_SYSTEM_POLYML]
   theories [document = false]
     "~~/src/HOL/Library/State_Monad"
     Code_Binary_Nat_examples
@@ -703,7 +702,7 @@
 
     TPTP-related extensions.
   *}
-  options [condition = ML_SYSTEM_POLYML, document = false]
+  options [document = false]
   theories
     ATP_Theory_Export
     MaSh_Eval
@@ -749,7 +748,7 @@
   theories Nominal
 
 session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
-  options [condition = ML_SYSTEM_POLYML, document = false]
+  options [document = false]
   theories
     Class3
     CK_Machine
@@ -838,11 +837,11 @@
   theories Mirabelle_Test
 
 session "HOL-Mirabelle-ex" in "Mirabelle/ex" = "HOL-Mirabelle" +
-  options [condition = ML_SYSTEM_POLYML, document = false, timeout = 60]
+  options [document = false, timeout = 60]
   theories Ex
 
 session "HOL-Word-SMT_Examples" in SMT_Examples = "HOL-Word" +
-  options [condition = ML_SYSTEM_POLYML, document = false, quick_and_dirty]
+  options [document = false, quick_and_dirty]
   theories
     Boogie
     SMT_Examples
@@ -981,7 +980,7 @@
 
 session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
   options [document = false]
-  theories [condition = ML_SYSTEM_POLYML]
+  theories
     Examples
     Predicate_Compile_Tests
     Predicate_Compile_Quickcheck_Examples
diff -r 7f927120b5a2 -r ab76bd43c14a src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -169,7 +169,6 @@
 fun alphanumerated_name prefix name =
   prefix ^ (raw_explode #> map alphanumerate #> implode) name
 
-(*SMLNJ complains if type annotation not used below*)
 fun mk_binding (config : config) ident =
   let
     val pre_binding = Binding.name (alphanumerated_name "bnd_" ident)
diff -r 7f927120b5a2 -r ab76bd43c14a src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -1609,10 +1609,8 @@
 
 (* values_timeout configuration *)
 
-val default_values_timeout = if ML_System.is_smlnj then 1200.0 else 40.0
-
 val values_timeout =
-  Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
+  Attrib.setup_config_real @{binding values_timeout} (K 40.0)
 
 val _ =
   Theory.setup
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/General/secure.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -13,7 +13,6 @@
   val use_text: use_context ->
     {line: int, file: string, verbose: bool, debug: bool} -> string -> unit
   val use_file: use_context -> {verbose: bool, debug: bool} -> string -> unit
-  val toplevel_pp: string list -> string -> unit
 end;
 
 structure Secure: SECURE =
@@ -36,11 +35,8 @@
 
 val raw_use_text = use_text;
 val raw_use_file = use_file;
-val raw_toplevel_pp = toplevel_pp;
 
 fun use_text context flags (text: string) = (secure_mltext (); raw_use_text context flags text);
 fun use_file context flags (file: string) = (secure_mltext (); raw_use_file context flags file);
 
-fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
-
 end;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/General/socket_io.ML
--- a/src/Pure/General/socket_io.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/General/socket_io.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -25,7 +25,7 @@
     val rd =
       BinPrimIO.RD {
         name = name,
-        chunkSize = io_buffer_size,
+        chunkSize = 4096,
         readVec = SOME (fn n => Socket.recvVec (socket, n)),
         readArr = SOME (fn buffer => Socket.recvArr (socket, buffer)),
         readVecNB = NONE,
@@ -44,7 +44,7 @@
     val wr =
       BinPrimIO.WR {
         name = name,
-        chunkSize = io_buffer_size,
+        chunkSize = 4096,
         writeVec = SOME (fn buffer => Socket.sendVec (socket, buffer)),
         writeArr = SOME (fn buffer => Socket.sendArr (socket, buffer)),
         writeVecNB = NONE,
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/exn_output.ML
--- a/src/Pure/ML/exn_output.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ML/exn_output.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -1,20 +1,24 @@
 (*  Title:      Pure/ML/exn_output.ML
     Author:     Makarius
 
-Auxiliary operations for exception output -- generic version.
+Auxiliary operations for exception output.
 *)
 
 signature EXN_OUTPUT =
 sig
   val position: exn -> Position.T
   val pretty: exn -> Pretty.T
-end
+end;
 
 structure Exn_Output: EXN_OUTPUT =
 struct
 
-fun position (_: exn) = Position.none
-val pretty = Pretty.str o General.exnMessage;
+fun position exn =
+  (case PolyML.exceptionLocation exn of
+    NONE => Position.none
+  | SOME loc => Exn_Properties.position_of loc);
+
+fun pretty (exn: exn) =
+  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
 
 end;
-
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/exn_output_polyml.ML
--- a/src/Pure/ML/exn_output_polyml.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      Pure/ML/exn_output_polyml.ML
-    Author:     Makarius
-
-Auxiliary operations for exception output -- Poly/ML version.
-*)
-
-structure Exn_Output: EXN_OUTPUT =
-struct
-
-fun position exn =
-  (case PolyML.exceptionLocation exn of
-    NONE => Position.none
-  | SOME loc => Exn_Properties.position_of loc);
-
-fun pretty (exn: exn) =
-  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
-
-end;
-
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/exn_properties.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_properties.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -0,0 +1,63 @@
+(*  Title:      Pure/ML/exn_properties.ML
+    Author:     Makarius
+
+Exception properties.
+*)
+
+signature EXN_PROPERTIES =
+sig
+  val position_of: PolyML.location -> Position.T
+  val get: exn -> Properties.T
+  val update: Properties.entry list -> exn -> exn
+end;
+
+structure Exn_Properties: EXN_PROPERTIES =
+struct
+
+(* source locations *)
+
+fun props_of (loc: PolyML.location) =
+  (case YXML.parse_body (#file loc) of
+    [] => []
+  | [XML.Text file] =>
+      if file = "Standard Basis" then []
+      else [(Markup.fileN, ml_standard_path file)]
+  | body => XML.Decode.properties body);
+
+fun position_of loc =
+  Position.make
+   {line = #startLine loc,
+    offset = #startPosition loc,
+    end_offset = #endPosition loc,
+    props = props_of loc};
+
+
+(* exception properties *)
+
+fun get exn =
+  (case PolyML.exceptionLocation exn of
+    NONE => []
+  | SOME loc => props_of loc);
+
+fun update entries exn =
+  let
+    val loc =
+      the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
+        (PolyML.exceptionLocation exn);
+    val props = props_of loc;
+    val props' = fold Properties.put entries props;
+  in
+    if props = props' then exn
+    else
+      let
+        val loc' =
+          {file = YXML.string_of_body (XML.Encode.properties props'),
+            startLine = #startLine loc, endLine = #endLine loc,
+            startPosition = #startPosition loc, endPosition = #endPosition loc};
+      in
+        uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
+          handle exn' => exn'
+      end
+  end;
+
+end;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/exn_properties_dummy.ML
--- a/src/Pure/ML/exn_properties_dummy.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(*  Title:      Pure/ML/exn_properties_dummy.ML
-    Author:     Makarius
-
-Exception properties -- dummy version.
-*)
-
-signature EXN_PROPERTIES =
-sig
-  val position_of: 'location -> Position.T
-  val get: exn -> Properties.T
-  val update: Properties.entry list -> exn -> exn
-end;
-
-structure Exn_Properties: EXN_PROPERTIES =
-struct
-
-fun position_of _ = Position.none;
-
-fun get _ = [];
-fun update _ exn = exn;
-
-end;
-
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/exn_properties_polyml.ML
--- a/src/Pure/ML/exn_properties_polyml.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-(*  Title:      Pure/ML/exn_properties_polyml.ML
-    Author:     Makarius
-
-Exception properties for Poly/ML.
-*)
-
-signature EXN_PROPERTIES =
-sig
-  val position_of: PolyML.location -> Position.T
-  val get: exn -> Properties.T
-  val update: Properties.entry list -> exn -> exn
-end;
-
-structure Exn_Properties: EXN_PROPERTIES =
-struct
-
-(* source locations *)
-
-fun props_of (loc: PolyML.location) =
-  (case YXML.parse_body (#file loc) of
-    [] => []
-  | [XML.Text file] =>
-      if file = "Standard Basis" then []
-      else [(Markup.fileN, ml_standard_path file)]
-  | body => XML.Decode.properties body);
-
-fun position_of loc =
-  Position.make
-   {line = #startLine loc,
-    offset = #startPosition loc,
-    end_offset = #endPosition loc,
-    props = props_of loc};
-
-
-(* exception properties *)
-
-fun get exn =
-  (case PolyML.exceptionLocation exn of
-    NONE => []
-  | SOME loc => props_of loc);
-
-fun update entries exn =
-  let
-    val loc =
-      the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
-        (PolyML.exceptionLocation exn);
-    val props = props_of loc;
-    val props' = fold Properties.put entries props;
-  in
-    if props = props' then exn
-    else
-      let
-        val loc' =
-          {file = YXML.string_of_body (XML.Encode.properties props'),
-            startLine = #startLine loc, endLine = #endLine loc,
-            startPosition = #startPosition loc, endPosition = #endPosition loc};
-      in
-        uninterruptible (fn _ => fn () => PolyML.raiseWithLocation (exn, loc')) ()
-          handle exn' => exn'
-      end
-  end;
-
-end;
-
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/install_pp_polyml.ML
--- a/src/Pure/ML/install_pp_polyml.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -1,9 +1,63 @@
 (*  Title:      Pure/ML/install_pp_polyml.ML
     Author:     Makarius
 
-Extra toplevel pretty-printing for Poly/ML.
+ML toplevel pretty-printing for Poly/ML.
 *)
 
+PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Pretty.T =>
+  ml_pretty (Pretty.to_ML (Pretty.str "<pretty>")));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn lexicon =>
+  ml_pretty (Pretty.to_ML (Lexicon.pp_lexicon lexicon)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn task =>
+  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_task task))));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn group =>
+  ml_pretty (Pretty.to_ML (Pretty.str (Task_Queue.str_of_group group))));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn pos =>
+  ml_pretty (Pretty.to_ML (Pretty.position pos)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn binding =>
+  ml_pretty (Pretty.to_ML (Binding.pp binding)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn th =>
+  ml_pretty (Pretty.to_ML (Proof_Display.pp_thm Thy_Info.pure_theory th)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn ct =>
+  ml_pretty (Pretty.to_ML (Proof_Display.pp_cterm Thy_Info.pure_theory ct)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn cT =>
+  ml_pretty (Pretty.to_ML (Proof_Display.pp_ctyp Thy_Info.pure_theory cT)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn T =>
+  ml_pretty (Pretty.to_ML (Proof_Display.pp_typ Thy_Info.pure_theory T)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn thy =>
+  ml_pretty (Pretty.to_ML (Context.pretty_thy thy)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn ctxt =>
+  ml_pretty (Pretty.to_ML (Proof_Display.pp_context ctxt)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn ast =>
+  ml_pretty (Pretty.to_ML (Ast.pretty_ast ast)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn path =>
+  ml_pretty (Pretty.to_ML (Path.pretty path)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn digest =>
+  ml_pretty (Pretty.to_ML (Pretty.str (quote (SHA1.rep digest)))));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn _: Proof.state =>
+  ml_pretty (Pretty.to_ML (Pretty.str "<Proof.state>")));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn st =>
+  ml_pretty (Pretty.to_ML (Toplevel.pretty_abstract st)));
+
+PolyML.addPrettyPrinter (fn _ => fn _ => fn morphism =>
+  ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
+
 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
   ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
 
@@ -107,4 +161,3 @@
 end;
 
 end;
-
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_compiler.ML
     Author:     Makarius
 
-Runtime compilation and evaluation -- generic version.
+Runtime compilation and evaluation.
 *)
 
 signature ML_COMPILER =
@@ -14,9 +14,12 @@
   val eval: flags -> Position.T -> ML_Lex.token list -> unit
 end
 
+
 structure ML_Compiler: ML_COMPILER =
 struct
 
+(* flags *)
+
 type flags =
   {SML: bool, exchange: bool, redirect: bool, verbose: bool,
     debug: bool option, writeln: string -> unit, warning: string -> unit};
@@ -29,16 +32,257 @@
   {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
     verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
 
+
+(* parse trees *)
+
+fun breakpoint_position loc =
+  let val pos = Position.reset_range (Exn_Properties.position_of loc) in
+    (case Position.offset_of pos of
+      NONE => pos
+    | SOME 1 => pos
+    | SOME j =>
+        Position.properties_of pos
+        |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
+        |> Position.of_properties)
+  end;
+
+fun report_parse_tree redirect depth space parse_tree =
+  let
+    val is_visible =
+      (case Context.thread_data () of
+        SOME context => Context_Position.is_visible_generic context
+      | NONE => true);
+    fun is_reported pos = is_visible andalso Position.is_reported pos;
+
+
+    (* syntax reports *)
+
+    fun reported_types loc types =
+      let val pos = Exn_Properties.position_of loc in
+        is_reported pos ?
+          let
+            val xml =
+              ML_Name_Space.displayTypeExpression (types, depth, space)
+              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+              |> Output.output |> YXML.parse_body;
+          in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
+      end;
+
+    fun reported_entity kind loc decl =
+      let
+        val pos = Exn_Properties.position_of loc;
+        val def_pos = Exn_Properties.position_of decl;
+      in
+        (is_reported pos andalso pos <> def_pos) ?
+          let
+            fun markup () =
+              (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
+          in cons (pos, markup, fn () => "") end
+      end;
+
+    fun reported_completions loc names =
+      let val pos = Exn_Properties.position_of loc in
+        if is_reported pos andalso not (null names) then
+          let
+            val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
+            val xml = Completion.encode completion;
+          in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
+        else I
+      end;
+
+    fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
+      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
+      | reported loc (PolyML.PTtype types) = reported_types loc types
+      | 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)
+    and reported_tree (loc, props) = fold (reported loc) props;
+
+    val persistent_reports = reported_tree parse_tree [];
+
+    fun output () =
+      persistent_reports
+      |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
+      |> Output.report;
+    val _ =
+      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
+      then
+        Execution.print
+          {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
+          output
+      else output ();
+
+
+    (* breakpoints *)
+
+    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)
+    and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
+
+    val all_breakpoints = rev (breakpoints_tree parse_tree []);
+    val _ = Position.reports (map #1 all_breakpoints);
+    val _ =
+      if is_some (Context.thread_data ()) then
+        Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints)
+      else ();
+  in () end;
+
+
+(* eval ML source tokens *)
+
 fun eval (flags: flags) pos toks =
   let
-    val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
-    val line = the_default 1 (Position.line_of pos);
-    val file = the_default "ML" (Position.file_of pos);
-    val debug = the_default false (#debug flags);
-    val text = ML_Lex.flatten toks;
+    val _ = Secure.secure_mltext ();
+    val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags};
+    val opt_context = Context.thread_data ();
+
+
+    (* input *)
+
+    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
+
+    val input_explode =
+      if #SML flags then String.explode
+      else maps (String.explode o Symbol.esc) o Symbol.explode;
+
+    val input_buffer =
+      Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of)));
+
+    fun get () =
+      (case ! input_buffer of
+        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
+      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
+      | [] => NONE);
+
+    fun get_pos () =
+      (case ! input_buffer of
+        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
+      | ([], tok) :: _ => ML_Lex.end_pos_of tok
+      | [] => Position.none);
+
+
+    (* output *)
+
+    val writeln_buffer = Unsynchronized.ref Buffer.empty;
+    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
+    fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer)));
+
+    val warnings = Unsynchronized.ref ([]: string list);
+    fun warn msg = Unsynchronized.change warnings (cons msg);
+    fun output_warnings () = List.app (#warning flags) (rev (! warnings));
+
+    val error_buffer = Unsynchronized.ref Buffer.empty;
+    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
+    fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
+    fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
+
+    fun message {message = msg, hard, location = loc, context = _} =
+      let
+        val pos = Exn_Properties.position_of loc;
+        val txt =
+          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
+          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
+      in if hard then err txt else warn txt end;
+
+
+    (* results *)
+
+    val depth = ML_Options.get_print_depth ();
+
+    fun apply_result {fixes, types, signatures, structures, functors, values} =
+      let
+        fun display disp x =
+          if depth > 0 then
+            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
+          else ();
+
+        fun apply_fix (a, b) =
+          (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
+        fun apply_type (a, b) =
+          (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
+        fun apply_sig (a, b) =
+          (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
+        fun apply_struct (a, b) =
+          (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
+        fun apply_funct (a, b) =
+          (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
+        fun apply_val (a, b) =
+          (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
+      in
+        List.app apply_fix fixes;
+        List.app apply_type types;
+        List.app apply_sig signatures;
+        List.app apply_struct structures;
+        List.app apply_funct functors;
+        List.app apply_val values
+      end;
+
+    exception STATIC_ERRORS of unit;
+
+    fun result_fun (phase1, phase2) () =
+     ((case phase1 of
+        NONE => ()
+      | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
+      (case phase2 of
+        NONE => raise STATIC_ERRORS ()
+      | SOME code =>
+          apply_result
+            ((code
+              |> Runtime.debugging opt_context
+              |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
+
+
+    (* compiler invocation *)
+
+    val debug =
+      (case #debug flags of
+        SOME debug => debug
+      | NONE => ML_Options.debugger_enabled opt_context);
+
+    val parameters =
+     [PolyML.Compiler.CPOutStream write,
+      PolyML.Compiler.CPNameSpace space,
+      PolyML.Compiler.CPErrorMessageProc message,
+      PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
+      PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
+      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;
+
+    val _ =
+      (while not (List.null (! input_buffer)) do
+        PolyML.compiler (get, parameters) ())
+      handle exn =>
+        if Exn.is_interrupt exn then reraise exn
+        else
+          let
+            val exn_msg =
+              (case exn of
+                STATIC_ERRORS () => ""
+              | Runtime.TOPLEVEL_ERROR => ""
+              | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
+            val _ = output_warnings ();
+            val _ = output_writeln ();
+          in raise_error exn_msg end;
   in
-    Secure.use_text ML_Env.local_context
-      {line = line, file = file, verbose = #verbose flags, debug = debug} text
+    if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
+    else ()
   end;
 
 end;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,265 +0,0 @@
-(*  Title:      Pure/ML/ml_compiler_polyml.ML
-    Author:     Makarius
-
-Runtime compilation and evaluation -- Poly/ML version.
-*)
-
-structure ML_Compiler: ML_COMPILER =
-struct
-
-open ML_Compiler;
-
-
-(* parse trees *)
-
-fun breakpoint_position loc =
-  let val pos = Position.reset_range (Exn_Properties.position_of loc) in
-    (case Position.offset_of pos of
-      NONE => pos
-    | SOME 1 => pos
-    | SOME j =>
-        Position.properties_of pos
-        |> Properties.put (Markup.offsetN, Markup.print_int (j - 1))
-        |> Position.of_properties)
-  end;
-
-fun report_parse_tree redirect depth space parse_tree =
-  let
-    val is_visible =
-      (case Context.thread_data () of
-        SOME context => Context_Position.is_visible_generic context
-      | NONE => true);
-    fun is_reported pos = is_visible andalso Position.is_reported pos;
-
-
-    (* syntax reports *)
-
-    fun reported_types loc types =
-      let val pos = Exn_Properties.position_of loc in
-        is_reported pos ?
-          let
-            val xml =
-              ML_Name_Space.displayTypeExpression (types, depth, space)
-              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
-              |> Output.output |> YXML.parse_body;
-          in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
-      end;
-
-    fun reported_entity kind loc decl =
-      let
-        val pos = Exn_Properties.position_of loc;
-        val def_pos = Exn_Properties.position_of decl;
-      in
-        (is_reported pos andalso pos <> def_pos) ?
-          let
-            fun markup () =
-              (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
-          in cons (pos, markup, fn () => "") end
-      end;
-
-    fun reported_completions loc names =
-      let val pos = Exn_Properties.position_of loc in
-        if is_reported pos andalso not (null names) then
-          let
-            val completion = Completion.names pos (map (fn a => (a, ("ML", a))) names);
-            val xml = Completion.encode completion;
-          in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
-        else I
-      end;
-
-    fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
-      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
-      | reported loc (PolyML.PTtype types) = reported_types loc types
-      | 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)
-    and reported_tree (loc, props) = fold (reported loc) props;
-
-    val persistent_reports = reported_tree parse_tree [];
-
-    fun output () =
-      persistent_reports
-      |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
-      |> Output.report;
-    val _ =
-      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
-      then
-        Execution.print
-          {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
-          output
-      else output ();
-
-
-    (* breakpoints *)
-
-    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)
-    and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
-
-    val all_breakpoints = rev (breakpoints_tree parse_tree []);
-    val _ = Position.reports (map #1 all_breakpoints);
-    val _ =
-      if is_some (Context.thread_data ()) then
-        Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints)
-      else ();
-  in () end;
-
-
-(* eval ML source tokens *)
-
-fun eval (flags: flags) pos toks =
-  let
-    val _ = Secure.secure_mltext ();
-    val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags};
-    val opt_context = Context.thread_data ();
-
-
-    (* input *)
-
-    val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
-
-    val input_explode =
-      if #SML flags then String.explode
-      else maps (String.explode o Symbol.esc) o Symbol.explode;
-
-    val input_buffer =
-      Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of)));
-
-    fun get () =
-      (case ! input_buffer of
-        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
-      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
-      | [] => NONE);
-
-    fun get_pos () =
-      (case ! input_buffer of
-        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
-      | ([], tok) :: _ => ML_Lex.end_pos_of tok
-      | [] => Position.none);
-
-
-    (* output *)
-
-    val writeln_buffer = Unsynchronized.ref Buffer.empty;
-    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
-    fun output_writeln () = #writeln flags (trim_line (Buffer.content (! writeln_buffer)));
-
-    val warnings = Unsynchronized.ref ([]: string list);
-    fun warn msg = Unsynchronized.change warnings (cons msg);
-    fun output_warnings () = List.app (#warning flags) (rev (! warnings));
-
-    val error_buffer = Unsynchronized.ref Buffer.empty;
-    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
-    fun flush_error () = #writeln flags (trim_line (Buffer.content (! error_buffer)));
-    fun raise_error msg = error (trim_line (Buffer.content (Buffer.add msg (! error_buffer))));
-
-    fun message {message = msg, hard, location = loc, context = _} =
-      let
-        val pos = Exn_Properties.position_of loc;
-        val txt =
-          (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
-          Pretty.string_of (Pretty.from_ML (pretty_ml msg));
-      in if hard then err txt else warn txt end;
-
-
-    (* results *)
-
-    val depth = ML_Options.get_print_depth ();
-
-    fun apply_result {fixes, types, signatures, structures, functors, values} =
-      let
-        fun display disp x =
-          if depth > 0 then
-            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
-          else ();
-
-        fun apply_fix (a, b) =
-          (#enterFix space (a, b); display ML_Name_Space.displayFix (a, b));
-        fun apply_type (a, b) =
-          (#enterType space (a, b); display ML_Name_Space.displayType (b, depth, space));
-        fun apply_sig (a, b) =
-          (#enterSig space (a, b); display ML_Name_Space.displaySig (b, depth, space));
-        fun apply_struct (a, b) =
-          (#enterStruct space (a, b); display ML_Name_Space.displayStruct (b, depth, space));
-        fun apply_funct (a, b) =
-          (#enterFunct space (a, b); display ML_Name_Space.displayFunct (b, depth, space));
-        fun apply_val (a, b) =
-          (#enterVal space (a, b); display ML_Name_Space.displayVal (b, depth, space));
-      in
-        List.app apply_fix fixes;
-        List.app apply_type types;
-        List.app apply_sig signatures;
-        List.app apply_struct structures;
-        List.app apply_funct functors;
-        List.app apply_val values
-      end;
-
-    exception STATIC_ERRORS of unit;
-
-    fun result_fun (phase1, phase2) () =
-     ((case phase1 of
-        NONE => ()
-      | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
-      (case phase2 of
-        NONE => raise STATIC_ERRORS ()
-      | SOME code =>
-          apply_result
-            ((code
-              |> Runtime.debugging opt_context
-              |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
-
-
-    (* compiler invocation *)
-
-    val debug =
-      (case #debug flags of
-        SOME debug => debug
-      | NONE => ML_Options.debugger_enabled opt_context);
-
-    val parameters =
-     [PolyML.Compiler.CPOutStream write,
-      PolyML.Compiler.CPNameSpace space,
-      PolyML.Compiler.CPErrorMessageProc message,
-      PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
-      PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
-      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;
-
-    val _ =
-      (while not (List.null (! input_buffer)) do
-        PolyML.compiler (get, parameters) ())
-      handle exn =>
-        if Exn.is_interrupt exn then reraise exn
-        else
-          let
-            val exn_msg =
-              (case exn of
-                STATIC_ERRORS () => ""
-              | Runtime.TOPLEVEL_ERROR => ""
-              | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
-            val _ = output_warnings ();
-            val _ = output_writeln ();
-          in raise_error exn_msg end;
-  in
-    if #verbose flags then (output_warnings (); flush_error (); output_writeln ())
-    else ()
-  end;
-
-end;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ML/ml_env.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -163,8 +163,7 @@
   end;
 
 val local_context: use_context =
- {tune_source = ML_Parse.fix_ints,
-  name_space = name_space {SML = false, exchange = false},
+ {name_space = name_space {SML = false, exchange = false},
   str_of_pos = Position.here oo Position.line_file,
   print = writeln,
   error = error};
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ML/ml_parse.ML
--- a/src/Pure/ML/ml_parse.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ML/ml_parse.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -6,7 +6,6 @@
 
 signature ML_PARSE =
 sig
-  val fix_ints: string -> string
   val global_context: use_context
 end;
 
@@ -43,30 +42,10 @@
 val blanks = Scan.repeat improper >> implode;
 
 
-(* fix_ints *)
-
-(*approximation only -- corrupts numeric record field patterns *)
-val fix_int =
-  $$$ "#" ^^ blanks ^^ int ||
-  ($$$ "infix" || $$$ "infixr") ^^ blanks ^^ int ||
-  int >> (fn x => "(" ^ x ^ ":int)") ||
-  regular ||
-  bad_input;
-
-val fix_ints =
-  ML_System.is_smlnj ?
-   (Source.of_string #>
-    ML_Lex.source #>
-    Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) #>
-    Source.exhaust #>
-    implode);
-
-
 (* global use_context *)
 
 val global_context: use_context =
- {tune_source = fix_ints,
-  name_space = ML_Name_Space.global,
+ {name_space = ML_Name_Space.global,
   str_of_pos = Position.here oo Position.line_file,
   print = writeln,
   error = error};
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -102,8 +102,6 @@
 val raw_explode = SML90.explode;
 val implode = SML90.implode;
 
-val io_buffer_size = 4096;
-
 fun quit () = exit 0;
 
 
@@ -191,10 +189,6 @@
 if ML_System.name = "polyml-5.6"
 then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
 
-fun toplevel_pp context (_: string list) pp =
-  use_text context {line = 1, file = "pp", verbose = false, debug = false}
-    ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
-
 fun ml_make_string struct_name =
   "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
     struct_name ^ ".ML_print_depth ())))))";
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/ROOT_smlnj.ML
--- a/src/Pure/RAW/ROOT_smlnj.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,194 +0,0 @@
-(*  Title:      Pure/RAW/ROOT_smlnj.ML
-
-Compatibility file for Standard ML of New Jersey.
-*)
-
-val io_buffer_size = 4096;
-use "RAW/proper_int.ML";
-
-exception Interrupt;
-fun reraise exn = raise exn;
-
-fun exit rc = Posix.Process.exit (Word8.fromInt rc);
-fun quit () = exit 0;
-
-use "RAW/overloading_smlnj.ML";
-use "RAW/exn.ML";
-use "RAW/single_assignment.ML";
-use "RAW/universal.ML";
-use "RAW/thread_dummy.ML";
-use "RAW/multithreading.ML";
-use "RAW/ml_stack_dummy.ML";
-use "RAW/ml_pretty.ML";
-use "RAW/ml_name_space.ML";
-structure PolyML = struct end;
-use "RAW/pp_dummy.ML";
-use "RAW/use_context.ML";
-use "RAW/ml_positions.ML";
-
-
-val seconds = Time.fromReal;
-
-(*low-level pointer equality*)
-CM.autoload "$smlnj/init/init.cmi";
-val pointer_eq = InlineT.ptreql;
-
-
-(* restore old-style character / string functions *)
-
-val ord = mk_int o SML90.ord;
-val chr = SML90.chr o dest_int;
-val raw_explode = SML90.explode;
-val implode = SML90.implode;
-
-
-(* New Jersey ML parameters *)
-
-val _ =
- (Control.Print.printLength := 1000;
-  Control.Print.printDepth := 350;
-  Control.Print.stringDepth := 250;
-  Control.Print.signatures := 2;
-  Control.MC.matchRedundantError := false);
-
-
-(* Poly/ML emulation *)
-
-(*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
-local
-  val depth = ref (10: int);
-in
-  fun get_default_print_depth () = ! depth;
-  fun default_print_depth n =
-   (depth := n;
-    Control.Print.printDepth := dest_int n div 2;
-    Control.Print.printLength := dest_int n);
-  val _ = default_print_depth 10;
-end;
-
-fun ml_make_string (_: string) = "(fn _ => \"?\")";
-
-
-(*prompts*)
-fun ml_prompts p1 p2 =
-  (Control.primaryPrompt := p1; Control.secondaryPrompt := p2);
-
-(*dummy implementation*)
-structure ML_Profiling =
-struct
-  fun profile_time (_: (int * string) list -> unit) f x = f x;
-  fun profile_time_thread (_: (int * string) list -> unit) f x = f x;
-  fun profile_allocations (_: (int * string) list -> unit) f x = f x;
-end;
-
-(*dummy implementation*)
-fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
-
-
-(* ML command execution *)
-
-fun use_text ({tune_source, print, error, ...}: use_context)
-    {line, file, verbose, debug = _: bool} text =
-  let
-    val ref out_orig = Control.Print.out;
-
-    val out_buffer = ref ([]: string list);
-    val out = {say = (fn s => out_buffer := s :: ! out_buffer), flush = (fn () => ())};
-    fun output () =
-      let val str = implode (rev (! out_buffer))
-      in String.substring (str, 0, Int.max (0, size str - 1)) end;
-  in
-    Control.Print.out := out;
-    Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file text)))
-      handle exn =>
-        (Control.Print.out := out_orig;
-          error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
-    Control.Print.out := out_orig;
-    if verbose then print (output ()) else ()
-  end;
-
-fun use_file context {verbose, debug} file =
-  let
-    val instream = TextIO.openIn file;
-    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
-
-
-(* toplevel pretty printing *)
-
-fun ml_pprint pps =
-  let
-    fun str "" = ()
-      | str s = PrettyPrint.string pps s;
-    fun pprint (ML_Pretty.Block ((bg, en), consistent, ind, prts)) =
-         (str bg;
-          (if consistent then PrettyPrint.openHVBox else PrettyPrint.openHOVBox) pps
-            (PrettyPrint.Rel (dest_int ind));
-          List.app pprint prts; PrettyPrint.closeBox pps;
-          str en)
-      | pprint (ML_Pretty.String (s, _)) = str s
-      | pprint (ML_Pretty.Break (false, width, offset)) =
-          PrettyPrint.break pps {nsp = dest_int width, offset = dest_int offset}
-      | pprint (ML_Pretty.Break (true, _, _)) = PrettyPrint.newline pps;
-  in pprint end;
-
-fun toplevel_pp context path pp =
-  use_text context {line = 1, file = "pp", verbose = false, debug = false}
-    ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
-      "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
-
-
-
-(** interrupts **)
-
-local
-
-fun change_signal new_handler f x =
-  let
-    val old_handler = Signals.setHandler (Signals.sigINT, new_handler);
-    val result = Exn.capture (f old_handler) x;
-    val _ = Signals.setHandler (Signals.sigINT, old_handler);
-  in Exn.release result end;
-
-in
-
-fun interruptible (f: 'a -> 'b) x =
-  let
-    val result = ref (Exn.interrupt_exn: 'b Exn.result);
-    val old_handler = Signals.inqHandler Signals.sigINT;
-  in
-    SMLofNJ.Cont.callcc (fn cont =>
-      (Signals.setHandler (Signals.sigINT, Signals.HANDLER (fn _ => cont));
-        result := Exn.capture f x));
-    Signals.setHandler (Signals.sigINT, old_handler);
-    Exn.release (! result)
-  end;
-
-fun uninterruptible f =
-  change_signal Signals.IGNORE
-    (fn old_handler => f (fn g => change_signal old_handler (fn _ => g)));
-
-end;
-
-
-use "RAW/unsynchronized.ML";
-use "RAW/ml_debugger.ML";
-
-
-(* ML system operations *)
-
-fun ml_platform_path (s: string) = s;
-fun ml_standard_path (s: string) = s;
-
-use "RAW/ml_system.ML";
-
-structure ML_System =
-struct
-
-open ML_System;
-
-fun save_state name =
-  if SMLofNJ.exportML name then ()
-  else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
-
-end;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/compiler_polyml.ML
--- a/src/Pure/RAW/compiler_polyml.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/RAW/compiler_polyml.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -11,12 +11,11 @@
 
 in
 
-fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+fun use_text ({name_space, str_of_pos, print, error, ...}: use_context)
     {line, file, verbose, debug} text =
   let
     val current_line = Unsynchronized.ref line;
-    val in_buffer =
-      Unsynchronized.ref (String.explode (tune_source (ml_positions line file text)));
+    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
     val out_buffer = Unsynchronized.ref ([]: string list);
     fun output () = drop_newline (implode (rev (! out_buffer)));
 
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/ml_name_space.ML
--- a/src/Pure/RAW/ml_name_space.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(*  Title:      Pure/RAW/ml_name_space.ML
-    Author:     Makarius
-
-ML name space -- dummy version of Poly/ML 5.2 facility.
-*)
-
-structure ML_Name_Space =
-struct
-
-type valueVal = unit;
-type typeVal = unit;
-type fixityVal = unit;
-type structureVal = unit;
-type signatureVal = unit;
-type functorVal = unit;
-
-type T =
- {lookupVal:    string -> valueVal option,
-  lookupType:   string -> typeVal option,
-  lookupFix:    string -> fixityVal option,
-  lookupStruct: string -> structureVal option,
-  lookupSig:    string -> signatureVal option,
-  lookupFunct:  string -> functorVal option,
-  enterVal:     string * valueVal -> unit,
-  enterType:    string * typeVal -> unit,
-  enterFix:     string * fixityVal -> unit,
-  enterStruct:  string * structureVal -> unit,
-  enterSig:     string * signatureVal -> unit,
-  enterFunct:   string * functorVal -> unit,
-  allVal:       unit -> (string * valueVal) list,
-  allType:      unit -> (string * typeVal) list,
-  allFix:       unit -> (string * fixityVal) list,
-  allStruct:    unit -> (string * structureVal) list,
-  allSig:       unit -> (string * signatureVal) list,
-  allFunct:     unit -> (string * functorVal) list};
-
-val global: T =
- {lookupVal = fn _ => NONE,
-  lookupType = fn _ => NONE,
-  lookupFix = fn _ => NONE,
-  lookupStruct = fn _ => NONE,
-  lookupSig = fn _ => NONE,
-  lookupFunct = fn _ => NONE,
-  enterVal = fn _ => (),
-  enterType = fn _ => (),
-  enterFix = fn _ => (),
-  enterStruct = fn _ => (),
-  enterSig = fn _ => (),
-  enterFunct = fn _ => (),
-  allVal = fn _ => [],
-  allType = fn _ => [],
-  allFix = fn _ => [],
-  allStruct = fn _ => [],
-  allSig = fn _ => [],
-  allFunct = fn _ => []};
-
-val initial_val : (string * valueVal) list = [];
-val initial_type : (string * typeVal) list = [];
-val initial_fixity : (string * fixityVal) list = [];
-val initial_structure : (string * structureVal) list = [];
-val initial_signature : (string * signatureVal) list = [];
-val initial_functor : (string * functorVal) list = [];
-
-fun forget_global_structure (_: string) = ();
-
-fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1);
-
-end;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/ml_system.ML
--- a/src/Pure/RAW/ml_system.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/RAW/ml_system.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -7,8 +7,6 @@
 signature ML_SYSTEM =
 sig
   val name: string
-  val is_polyml: bool
-  val is_smlnj: bool
   val platform: string
   val platform_is_windows: bool
   val share_common_data: unit -> unit
@@ -19,8 +17,6 @@
 struct
 
 val SOME name = OS.Process.getEnv "ML_SYSTEM";
-val is_polyml = String.isPrefix "polyml" name;
-val is_smlnj = String.isPrefix "smlnj" name;
 
 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
 val platform_is_windows = String.isSuffix "windows" platform;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/overloading_smlnj.ML
--- a/src/Pure/RAW/overloading_smlnj.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      Pure/RAW/overloading_smlnj.ML
-    Author:     Makarius
-
-Overloading in SML/NJ (cf. smlnj/base/system/smlnj/init/pervasive.sml).
-*)
-
-Control.overloadKW := true;
-
-overload ~ : ('a -> 'a) as
-  IntInf.~ and Int31.~ and Int32.~ and Int64.~ and
-  Word.~ and Word8.~ and Word32.~ and Word64.~ and Real.~;
-overload + : ('a * 'a -> 'a) as
-  IntInf.+ and Int31.+ and Int32.+ and Int64.+ and
-  Word.+ and Word8.+ and Word32.+ and Word64.+ and Real.+;
-overload - : ('a * 'a -> 'a) as
-  IntInf.- and Int31.- and Int32.- and Int64.- and
-  Word.- and Word8.- and Word32.- and Word64.- and Real.-;
-overload * : ('a * 'a -> 'a) as
-  IntInf.* and Int31.* and Int32.* and Int64.* and
-  Word.* and Word8.* and Word32.* and Word64.* and Real.*;
-overload div: ('a * 'a -> 'a) as
-  IntInf.div and Int31.div and Int32.div and Int64.div and
-  Word.div and Word8.div and Word32.div and Word64.div;
-overload mod: ('a * 'a -> 'a) as
-  IntInf.mod and Int31.mod and Int32.mod and Int64.mod and
-  Word.mod and Word8.mod and Word32.mod and Word64.mod;
-overload < : ('a * 'a -> bool) as
-  IntInf.< and Int31.< and Int32.< and Int64.< and Real.< and
-  Word.< and Word8.< and Word32.< and Word64.< and Char.< and String.<;
-overload <= : ('a * 'a -> bool) as
-  IntInf.<= and Int31.<= and Int32.<= and Int64.<= and Real.<= and
-  Word.<= and Word8.<= and Word32.<= and Word64.<= and Char.<= and String.<=;
-overload > : ('a * 'a -> bool) as
-  IntInf.> and Int31.> and Int32.> and Int64.> and Real.> and
-  Word.> and Word8.> and Word32.> and Word64.> and Char.> and String.>;
-overload >= : ('a * 'a -> bool) as
-  IntInf.>= and Int31.>= and Int32.>= and Int64.>= and Real.>= and
-  Word.>= and Word8.>= and Word32.>= and Word64.>= and Char.>= and String.>=;
-overload abs: ('a -> 'a) as IntInf.abs and Int31.abs and Int32.abs and Int64.abs and Real.abs;
-
-Control.overloadKW := false;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/pp_dummy.ML
--- a/src/Pure/RAW/pp_dummy.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/RAW/pp_dummy.ML
-
-Dummy setup for toplevel pretty printing.
-*)
-
-fun ml_pretty _ = raise Fail "ml_pretty dummy";
-fun pretty_ml _ = raise Fail "pretty_ml dummy";
-
-structure PolyML =
-struct
-  fun addPrettyPrinter _ = ();
-  fun prettyRepresentation _ =
-    raise Fail "PolyML.prettyRepresentation dummy";
-  open PolyML;
-end;
-
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/proper_int.ML
--- a/src/Pure/RAW/proper_int.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,289 +0,0 @@
-(*  Title:      Pure/RAW/proper_int.ML
-    Author:     Makarius
-
-SML basis with type int representing proper integers, not machine
-words.
-*)
-
-val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
-val dest_int = IntInf.toInt: IntInf.int -> Int.int;
-
-
-(* Int *)
-
-type int = IntInf.int;
-
-structure IntInf =
-struct
-  open IntInf;
-  fun fromInt (a: int) = a;
-  fun toInt (a: int) = a;
-  val log2 = mk_int o IntInf.log2;
-  val sign = mk_int o IntInf.sign;
-end;
-
-structure Int = IntInf;
-
-
-(* List *)
-
-structure List =
-struct
-  open List;
-  fun length a = mk_int (List.length a);
-  fun nth (a, b) = List.nth (a, dest_int b);
-  fun take (a, b) = List.take (a, dest_int b);
-  fun drop (a, b) = List.drop (a, dest_int b);
-  fun tabulate (a, b) = List.tabulate (dest_int a, b o mk_int);
-end;
-
-val length = List.length;
-
-
-(* Array *)
-
-structure Array =
-struct
-  open Array;
-  val maxLen = mk_int Array.maxLen;
-  fun array (a, b) = Array.array (dest_int a, b);
-  fun tabulate (a, b) = Array.tabulate (dest_int a, b o mk_int);
-  fun length a = mk_int (Array.length a);
-  fun sub (a, b) = Array.sub (a, dest_int b);
-  fun update (a, b, c) = Array.update (a, dest_int b, c);
-  fun copy {src, dst, di} = Array.copy {src = src, dst = dst, di = dest_int di};
-  fun copyVec {src, dst, di} = Array.copyVec {src = src, dst = dst, di = dest_int di};
-  fun appi a b = Array.appi (fn (x, y) => a (mk_int x, y)) b;
-  fun modifyi a b = Array.modifyi (fn (x, y) => a (mk_int x, y)) b;
-  fun foldli a b c = Array.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
-  fun foldri a b c = Array.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
-  fun findi a b =
-    (case Array.findi (fn (x, y) => a (mk_int x, y)) b of
-      NONE => NONE
-    | SOME (c, d) => SOME (mk_int c, d));
-end;
-
-
-(* Vector *)
-
-structure Vector =
-struct
-  open Vector;
-  val maxLen = mk_int Vector.maxLen;
-  fun tabulate (a, b) = Vector.tabulate (dest_int a, b o mk_int);
-  fun length a = mk_int (Vector.length a);
-  fun sub (a, b) = Vector.sub (a, dest_int b);
-  fun update (a, b, c) = Vector.update (a, dest_int b, c);
-  fun appi a b = Vector.appi (fn (x, y) => a (mk_int x, y)) b;
-  fun mapi a b = Vector.mapi (fn (x, y) => a (mk_int x, y)) b;
-  fun foldli a b c = Vector.foldli (fn (x, y, z) => a (mk_int x, y, z)) b c;
-  fun foldri a b c = Vector.foldri (fn (x, y, z) => a (mk_int x, y, z)) b c;
-  fun findi a b =
-    (case Vector.findi (fn (x, y) => a (mk_int x, y)) b of
-      NONE => NONE
-    | SOME (c, d) => SOME (mk_int c, d));
-end;
-
-
-(* CharVector *)
-
-structure CharVector =
-struct
-  open CharVector;
-  fun tabulate (a, b) = CharVector.tabulate (dest_int a, b o mk_int);
-end;
-
-
-(* Word8VectorSlice *)
-
-structure Word8VectorSlice =
-struct
-  open Word8VectorSlice;
-  val length = mk_int o Word8VectorSlice.length;
-  fun subslice (a, b, c) = Word8VectorSlice.subslice (a, dest_int b, Option.map dest_int c);
-end;
-
-
-(* Char *)
-
-structure Char =
-struct
-  open Char;
-  val maxOrd = mk_int Char.maxOrd;
-  val chr = Char.chr o dest_int;
-  val ord = mk_int o Char.ord;
-end;
-
-val chr = Char.chr;
-val ord = Char.ord;
-
-
-(* String *)
-
-structure String =
-struct
-  open String;
-  val maxSize = mk_int String.maxSize;
-  val size = mk_int o String.size;
-  fun sub (a, b) = String.sub (a, dest_int b);
-  fun extract (a, b, c) = String.extract (a, dest_int b, Option.map dest_int c);
-  fun substring (a, b, c) = String.substring (a, dest_int b, dest_int c);
-end;
-
-val size = String.size;
-val substring = String.substring;
-
-
-(* Substring *)
-
-structure Substring =
-struct
-  open Substring;
-  fun sub (a, b) = Substring.sub (a, dest_int b);
-  val size = mk_int o Substring.size;
-  fun base a = let val (b, c, d) = Substring.base a in (b, mk_int c, mk_int d) end;
-  fun extract (a, b, c) = Substring.extract (a, dest_int b, Option.map dest_int c);
-  fun substring (a, b, c) = Substring.substring (a, dest_int b, dest_int c);
-  fun triml a b = Substring.triml (dest_int a) b;
-  fun trimr a b = Substring.trimr (dest_int a) b;
-  fun slice (a, b, c) = Substring.slice (a, dest_int b, Option.map dest_int c);
-  fun splitAt (a, b) = Substring.splitAt (a, dest_int b);
-end;
-
-
-(* StringCvt *)
-
-structure StringCvt =
-struct
-  open StringCvt;
-  datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option;
-  fun realfmt fmt = Real.fmt
-    (case fmt of
-      EXACT => StringCvt.EXACT
-    | FIX NONE => StringCvt.FIX NONE
-    | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
-    | GEN NONE => StringCvt.GEN NONE
-    | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
-    | SCI NONE => StringCvt.SCI NONE
-    | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
-  fun padRight a b c = StringCvt.padRight a (dest_int b) c;
-  fun padLeft a b c = StringCvt.padLeft a (dest_int b) c;
-end;
-
-
-(* Word *)
-
-structure Word =
-struct
-  open Word;
-  val wordSize = mk_int Word.wordSize;
-  val toInt = Word.toLargeInt;
-  val toIntX = Word.toLargeIntX;
-  val fromInt = Word.fromLargeInt;
-end;
-
-structure Word8 =
-struct
-  open Word8;
-  val wordSize = mk_int Word8.wordSize;
-  val toInt = Word8.toLargeInt;
-  val toIntX = Word8.toLargeIntX;
-  val fromInt = Word8.fromLargeInt;
-end;
-
-structure Word32 =
-struct
-  open Word32;
-  val wordSize = mk_int Word32.wordSize;
-  val toInt = Word32.toLargeInt;
-  val toIntX = Word32.toLargeIntX;
-  val fromInt = Word32.fromLargeInt;
-end;
-
-structure LargeWord =
-struct
-  open LargeWord;
-  val wordSize = mk_int LargeWord.wordSize;
-  val toInt = LargeWord.toLargeInt;
-  val toIntX = LargeWord.toLargeIntX;
-  val fromInt = LargeWord.fromLargeInt;
-end;
-
-
-(* Real *)
-
-structure Real =
-struct
-  open Real;
-  val radix = mk_int Real.radix;
-  val precision = mk_int Real.precision;
-  fun sign a = mk_int (Real.sign a);
-  fun toManExp a = let val {man, exp} = Real.toManExp a in {man = man, exp = mk_int exp} end;
-  fun fromManExp {man, exp} = Real.fromManExp {man = man, exp = dest_int exp};
-  val ceil = mk_int o Real.ceil;
-  val floor = mk_int o Real.floor;
-  val real = Real.fromInt o dest_int;
-  val round = mk_int o Real.round;
-  val trunc = mk_int o Real.trunc;
-  fun toInt a b = mk_int (Real.toInt a b);
-  fun fromInt a = Real.fromInt (dest_int a);
-  val fmt = StringCvt.realfmt;
-end;
-
-val ceil = Real.ceil;
-val floor = Real.floor;
-val real = Real.real;
-val round = Real.round;
-val trunc = Real.trunc;
-
-
-(* TextIO *)
-
-structure TextIO =
-struct
-  open TextIO;
-  fun inputN (a, b) = TextIO.inputN (a, dest_int b);
-  fun canInput (a, b) = Option.map mk_int (TextIO.canInput (a, dest_int b));
-end;
-
-
-(* BinIO *)
-
-structure BinIO =
-struct
-  open BinIO;
-  fun inputN (a, b) = BinIO.inputN (a, dest_int b);
-  fun canInput (a, b) = Option.map mk_int (BinIO.canInput (a, dest_int b));
-end;
-
-
-(* Time *)
-
-structure Time =
-struct
-  open Time;
-  fun fmt a b = Time.fmt (dest_int a) b;
-end;
-
-
-(* Sockets *)
-
-structure INetSock =
-struct
-  open INetSock;
-  fun toAddr (a, b) = INetSock.toAddr (a, dest_int b);
-  fun fromAddr adr = let val (a, b) = INetSock.fromAddr adr in (a, mk_int b) end;
-end;
-
-
-(* OS.FileSys *)
-
-structure OS =
-struct
-  open OS;
-  structure FileSys =
-  struct
-    open FileSys;
-    fun fileSize a = mk_int (FileSys.fileSize a);
-  end;
-end;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/single_assignment.ML
--- a/src/Pure/RAW/single_assignment.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title:      Pure/RAW/single_assignment.ML
-    Author:     Makarius
-
-References with single assignment.  Unsynchronized!
-*)
-
-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
-  | saset _ = raise Locked;
-
-end;
-
-end;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/thread_dummy.ML
--- a/src/Pure/RAW/thread_dummy.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-(*  Title:      Pure/RAW/thread_dummy.ML
-    Author:     Makarius
-
-Default (mostly dummy) implementation of thread structures
-(cf. polyml/basis/Thread.sml).
-*)
-
-exception Thread of string;
-
-local fun fail _ = raise Thread "No multithreading support on this ML platform" in
-
-structure Mutex =
-struct
-  type mutex = unit;
-  fun mutex _ = ();
-  fun lock _ = fail ();
-  fun unlock _ = fail ();
-  fun trylock _ = fail ();
-end;
-
-structure ConditionVar =
-struct
-  type conditionVar = unit;
-  fun conditionVar _ = ();
-  fun wait _ = fail ();
-  fun waitUntil _ = fail ();
-  fun signal _ = fail ();
-  fun broadcast _ = fail ();
-end;
-
-structure Thread =
-struct
-  type thread = unit;
-
-  datatype threadAttribute = EnableBroadcastInterrupt of bool | InterruptState of interruptState
-    and interruptState = InterruptDefer | InterruptSynch | InterruptAsynch | InterruptAsynchOnce;
-
-  fun unavailable () = fail ();
-
-  fun fork _ = fail ();
-  fun exit _ = fail ();
-  fun isActive _ = fail ();
-
-  fun equal _ = fail ();
-  fun self _ = fail ();
-
-  fun interrupt _ = fail ();
-  fun broadcastInterrupt _ = fail ();
-  fun testInterrupt _ = fail ();
-
-  fun kill _ = fail ();
-
-  fun setAttributes _ = fail ();
-  fun getAttributes _ = fail ();
-
-  fun numProcessors _ = fail ();
-
-
-(* thread data *)
-
-local
-
-val data = ref ([]: Universal.universal  ref list);
-
-fun find_data tag =
-  let
-    fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs
-      | find [] = NONE;
-  in find (! data) end;
-
-in
-
-fun getLocal tag = Option.map (Universal.tagProject tag o !) (find_data tag);
-
-fun setLocal (tag, x) =
-  (case find_data tag of
-    SOME r => r := Universal.tagInject tag x
-  | NONE => data :=  ref (Universal.tagInject tag x) :: ! data);
-
-end;
-end;
-end;
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/universal.ML
--- a/src/Pure/RAW/universal.ML	Wed Feb 17 21:51:58 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      Pure/RAW/universal.ML
-    Author:     Makarius
-
-Universal values via tagged union.  Emulates structure Universal
-from Poly/ML 5.1.
-*)
-
-signature UNIVERSAL =
-sig
-  type universal
-  type 'a tag
-  val tag: unit -> 'a tag
-  val tagIs: 'a tag -> universal -> bool
-  val tagInject: 'a tag -> 'a -> universal
-  val tagProject: 'a tag -> universal -> 'a
-end;
-
-structure Universal: UNIVERSAL =
-struct
-
-type universal = exn;
-
-datatype 'a tag = Tag of
- {is: universal -> bool,
-  inject: 'a -> universal,
-  project: universal -> 'a};
-
-fun tag () =
-  let exception Universal of 'a in
-   Tag {
-    is = fn Universal _ => true | _ => false,
-    inject = Universal,
-    project = fn Universal x => x}
-  end;
-
-fun tagIs (Tag {is, ...}) = is;
-fun tagInject (Tag {inject, ...}) = inject;
-fun tagProject (Tag {project, ...}) = project;
-
-end;
-
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/RAW/use_context.ML
--- a/src/Pure/RAW/use_context.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/RAW/use_context.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -5,8 +5,7 @@
 *)
 
 type use_context =
- {tune_source: string -> string,
-  name_space: ML_Name_Space.T,
+ {name_space: ML_Name_Space.T,
   str_of_pos: int -> string -> string,
   print: string -> unit,
   error: string -> unit};
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ROOT	Wed Feb 17 23:29:35 2016 +0100
@@ -6,7 +6,6 @@
     "RAW/ROOT_polyml-5.5.2.ML"
     "RAW/ROOT_polyml-5.6.ML"
     "RAW/ROOT_polyml.ML"
-    "RAW/ROOT_smlnj.ML"
     "RAW/compiler_polyml.ML"
     "RAW/exn.ML"
     "RAW/exn_trace_polyml-5.5.1.ML"
@@ -14,7 +13,6 @@
     "RAW/ml_compiler_parameters_polyml-5.6.ML"
     "RAW/ml_debugger.ML"
     "RAW/ml_debugger_polyml-5.6.ML"
-    "RAW/ml_name_space.ML"
     "RAW/ml_name_space_polyml-5.6.ML"
     "RAW/ml_name_space_polyml.ML"
     "RAW/ml_parse_tree.ML"
@@ -28,14 +26,8 @@
     "RAW/ml_system.ML"
     "RAW/multithreading.ML"
     "RAW/multithreading_polyml.ML"
-    "RAW/overloading_smlnj.ML"
-    "RAW/pp_dummy.ML"
-    "RAW/proper_int.ML"
     "RAW/share_common_data_polyml-5.3.0.ML"
-    "RAW/single_assignment.ML"
     "RAW/single_assignment_polyml.ML"
-    "RAW/thread_dummy.ML"
-    "RAW/universal.ML"
     "RAW/unsynchronized.ML"
     "RAW/use_context.ML"
     "RAW/windows_path.ML"
@@ -46,7 +38,6 @@
     "RAW/ROOT_polyml-5.5.2.ML"
     "RAW/ROOT_polyml-5.6.ML"
     "RAW/ROOT_polyml.ML"
-    "RAW/ROOT_smlnj.ML"
     "RAW/compiler_polyml.ML"
     "RAW/exn.ML"
     "RAW/exn_trace_polyml-5.5.1.ML"
@@ -54,7 +45,6 @@
     "RAW/ml_compiler_parameters_polyml-5.6.ML"
     "RAW/ml_debugger.ML"
     "RAW/ml_debugger_polyml-5.6.ML"
-    "RAW/ml_name_space.ML"
     "RAW/ml_name_space_polyml-5.6.ML"
     "RAW/ml_name_space_polyml.ML"
     "RAW/ml_parse_tree.ML"
@@ -68,14 +58,8 @@
     "RAW/ml_system.ML"
     "RAW/multithreading.ML"
     "RAW/multithreading_polyml.ML"
-    "RAW/overloading_smlnj.ML"
-    "RAW/pp_dummy.ML"
-    "RAW/proper_int.ML"
     "RAW/share_common_data_polyml-5.3.0.ML"
-    "RAW/single_assignment.ML"
     "RAW/single_assignment_polyml.ML"
-    "RAW/thread_dummy.ML"
-    "RAW/universal.ML"
     "RAW/unsynchronized.ML"
     "RAW/use_context.ML"
     "RAW/windows_path.ML"
@@ -180,13 +164,10 @@
     "Isar/toplevel.ML"
     "Isar/typedecl.ML"
     "ML/exn_output.ML"
-    "ML/exn_output_polyml.ML"
-    "ML/exn_properties_dummy.ML"
-    "ML/exn_properties_polyml.ML"
+    "ML/exn_properties.ML"
     "ML/install_pp_polyml.ML"
     "ML/ml_antiquotation.ML"
     "ML/ml_compiler.ML"
-    "ML/ml_compiler_polyml.ML"
     "ML/ml_context.ML"
     "ML/ml_env.ML"
     "ML/ml_file.ML"
diff -r 7f927120b5a2 -r ab76bd43c14a src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Pure/ROOT.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -47,8 +47,6 @@
       Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
         handle ERROR msg => (writeln msg; error "ML error")) ();
 
-val toplevel_pp = Secure.toplevel_pp;
-
 
 
 (** bootstrap phase 1: towards ML within Isar context *)
@@ -76,7 +74,7 @@
 use "General/timing.ML";
 
 use "General/sha1.ML";
-if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
+use "General/sha1_polyml.ML";
 use "General/sha1_samples.ML";
 
 use "PIDE/yxml.ML";
@@ -98,9 +96,7 @@
 
 (* concurrency within the ML runtime *)
 
-if ML_System.is_polyml
-then use "ML/exn_properties_polyml.ML"
-else use "ML/exn_properties_dummy.ML";
+use "ML/exn_properties.ML";
 
 if ML_System.name = "polyml-5.5.0"
   orelse ML_System.name = "polyml-5.5.1"
@@ -123,8 +119,7 @@
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
 use "Concurrent/event_timer.ML";
-
-if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
+use "Concurrent/time_limit.ML";
 
 use "Concurrent/lazy.ML";
 if Multithreading.available then ()
@@ -204,12 +199,10 @@
 use "ML/ml_env.ML";
 use "ML/ml_options.ML";
 use "ML/exn_output.ML";
-if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
 use "ML/ml_options.ML";
 use "Isar/runtime.ML";
 use "PIDE/execution.ML";
 use "ML/ml_compiler.ML";
-if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
 
 use "skip_proof.ML";
 use "goal.ML";
@@ -338,28 +331,7 @@
 structure Output: OUTPUT = Output;  (*seal system channels!*)
 
 
-(* ML toplevel pretty printing *)
-
-toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
-toplevel_pp ["Scan", "lexicon"] "Lexicon.pp_lexicon";
-toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
-toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
-toplevel_pp ["Position", "T"] "Pretty.position";
-toplevel_pp ["Binding", "binding"] "Binding.pp";
-toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm Thy_Info.pure_theory";
-toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm Thy_Info.pure_theory";
-toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp Thy_Info.pure_theory";
-toplevel_pp ["typ"] "Proof_Display.pp_typ Thy_Info.pure_theory";
-toplevel_pp ["Context", "theory"] "Context.pretty_thy";
-toplevel_pp ["Context", "Proof", "context"] "Proof_Display.pp_context";
-toplevel_pp ["Ast", "ast"] "Ast.pretty_ast";
-toplevel_pp ["Path", "T"] "Path.pretty";
-toplevel_pp ["SHA1", "digest"] "Pretty.str o quote o SHA1.rep";
-toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
-toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
-toplevel_pp ["Morphism", "morphism"] "Morphism.pretty";
-
-if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
+use "ML/install_pp_polyml.ML";
 
 
 (* the Pure theory *)
diff -r 7f927120b5a2 -r ab76bd43c14a src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -510,8 +510,7 @@
 fun abort _ = error "Only value bindings allowed.";
 
 val notifying_context : use_context =
- {tune_source = #tune_source ML_Env.local_context,
-  name_space =
+ {name_space =
    {lookupVal    = #lookupVal ML_Env.local_name_space,
     lookupType   = #lookupType ML_Env.local_name_space,
     lookupFix    = #lookupFix ML_Env.local_name_space,
diff -r 7f927120b5a2 -r ab76bd43c14a src/Tools/ROOT
--- a/src/Tools/ROOT	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Tools/ROOT	Wed Feb 17 23:29:35 2016 +0100
@@ -1,11 +1,8 @@
 session Spec_Check in Spec_Check = Pure +
   theories
     Spec_Check
-  theories [condition = ML_SYSTEM_POLYML]
     Examples
 
 session SML in SML = Pure +
-  options [condition = ML_SYSTEM_POLYML]
   theories
     Examples
-
diff -r 7f927120b5a2 -r ab76bd43c14a src/Tools/Spec_Check/spec_check.ML
--- a/src/Tools/Spec_Check/spec_check.ML	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/Tools/Spec_Check/spec_check.ML	Wed Feb 17 23:29:35 2016 +0100
@@ -128,8 +128,7 @@
   let
     val return = Unsynchronized.ref "return"
     val use_context : use_context =
-     {tune_source = #tune_source ML_Env.local_context,
-      name_space = #name_space ML_Env.local_context,
+     {name_space = #name_space ML_Env.local_context,
       str_of_pos = #str_of_pos ML_Env.local_context,
       print = fn r => return := r,
       error = #error ML_Env.local_context}