# HG changeset patch
# User wenzelm
# Date 1455746784 -3600
# Node ID fdd6989cc8a09c0bed7136c0fa60ed3dcc30bb29
# Parent  a594429637fdf018b1f6582bceb7b55ddef588aa
SML/NJ is no longer supported;

diff -r a594429637fd -r fdd6989cc8a0 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Wed Feb 17 21:08:18 2016 +0100
+++ b/Admin/Release/CHECKLIST	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Wed Feb 17 21:08:18 2016 +0100
+++ b/Admin/isatest/isatest-makeall	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Wed Feb 17 21:08:18 2016 +0100
+++ b/Admin/isatest/isatest-makedist	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 Admin/isatest/isatest-stats
--- a/Admin/isatest/isatest-stats	Wed Feb 17 21:08:18 2016 +0100
+++ b/Admin/isatest/isatest-stats	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 Admin/isatest/settings/at-sml-dev-e
--- a/Admin/isatest/settings/at-sml-dev-e	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 NEWS
--- a/NEWS	Wed Feb 17 21:08:18 2016 +0100
+++ b/NEWS	Wed Feb 17 23:06:24 2016 +0100
@@ -33,6 +33,12 @@
     INCOMPATIBILITY.
 
 
+*** System ***
+
+* SML/NJ is no longer supported.
+
+
+
 New in Isabelle2016 (February 2016)
 -----------------------------------
 
diff -r a594429637fd -r fdd6989cc8a0 etc/settings
--- a/etc/settings	Wed Feb 17 21:08:18 2016 +0100
+++ b/etc/settings	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Wed Feb 17 21:08:18 2016 +0100
+++ b/lib/scripts/getsettings	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Doc/Implementation/ML.thy	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Doc/ROOT
--- a/src/Doc/ROOT	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Doc/ROOT	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Doc/System/Basics.thy
--- a/src/Doc/System/Basics.thy	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Doc/System/Basics.thy	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/ROOT	Wed Feb 17 23:06:24 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
@@ -245,24 +245,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 +
@@ -394,11 +394,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
@@ -407,7 +407,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"
@@ -432,7 +432,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"
@@ -531,7 +531,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
@@ -702,7 +701,7 @@
 
     TPTP-related extensions.
   *}
-  options [condition = ML_SYSTEM_POLYML, document = false]
+  options [document = false]
   theories
     ATP_Theory_Export
     MaSh_Eval
@@ -748,7 +747,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
@@ -837,11 +836,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
@@ -980,7 +979,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 a594429637fd -r fdd6989cc8a0 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Pure/General/socket_io.ML
--- a/src/Pure/General/socket_io.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/General/socket_io.ML	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Pure/ML/exn_output.ML
--- a/src/Pure/ML/exn_output.ML	Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*  Title:      Pure/ML/exn_output.ML
-    Author:     Makarius
-
-Auxiliary operations for exception output -- generic version.
-*)
-
-signature EXN_OUTPUT =
-sig
-  val position: exn -> Position.T
-  val pretty: exn -> Pretty.T
-end
-
-structure Exn_Output: EXN_OUTPUT =
-struct
-
-fun position (_: exn) = Position.none
-val pretty = Pretty.str o General.exnMessage;
-
-end;
-
diff -r a594429637fd -r fdd6989cc8a0 src/Pure/ML/exn_output_polyml.ML
--- a/src/Pure/ML/exn_output_polyml.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ML/exn_output_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
@@ -4,6 +4,12 @@
 Auxiliary operations for exception output -- Poly/ML version.
 *)
 
+signature EXN_OUTPUT =
+sig
+  val position: exn -> Position.T
+  val pretty: exn -> Pretty.T
+end;
+
 structure Exn_Output: EXN_OUTPUT =
 struct
 
@@ -16,4 +22,3 @@
   Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
 
 end;
-
diff -r a594429637fd -r fdd6989cc8a0 src/Pure/ML/exn_properties_dummy.ML
--- a/src/Pure/ML/exn_properties_dummy.ML	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Feb 17 21:08:18 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(*  Title:      Pure/ML/ml_compiler.ML
-    Author:     Makarius
-
-Runtime compilation and evaluation -- generic version.
-*)
-
-signature ML_COMPILER =
-sig
-  type flags =
-    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
-      debug: bool option, writeln: string -> unit, warning: string -> unit}
-  val flags: flags
-  val verbose: bool -> flags -> flags
-  val eval: flags -> Position.T -> ML_Lex.token list -> unit
-end
-
-structure ML_Compiler: ML_COMPILER =
-struct
-
-type flags =
-  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
-    debug: bool option, writeln: string -> unit, warning: string -> unit};
-
-val flags: flags =
-  {SML = false, exchange = false, redirect = false, verbose = false,
-    debug = NONE, writeln = writeln, warning = warning};
-
-fun verbose b (flags: flags) =
-  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
-    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
-
-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;
-  in
-    Secure.use_text ML_Env.local_context
-      {line = line, file = file, verbose = #verbose flags, debug = debug} text
-  end;
-
-end;
diff -r a594429637fd -r fdd6989cc8a0 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
@@ -4,10 +4,33 @@
 Runtime compilation and evaluation -- Poly/ML version.
 *)
 
+signature ML_COMPILER =
+sig
+  type flags =
+    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+      debug: bool option, writeln: string -> unit, warning: string -> unit}
+  val flags: flags
+  val verbose: bool -> flags -> flags
+  val eval: flags -> Position.T -> ML_Lex.token list -> unit
+end
+
+
 structure ML_Compiler: ML_COMPILER =
 struct
 
-open ML_Compiler;
+(* flags *)
+
+type flags =
+  {SML: bool, exchange: bool, redirect: bool, verbose: bool,
+    debug: bool option, writeln: string -> unit, warning: string -> unit};
+
+val flags: flags =
+  {SML = false, exchange = false, redirect = false, verbose = false,
+    debug = NONE, writeln = writeln, warning = warning};
+
+fun verbose b (flags: flags) =
+  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
+    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
 
 
 (* parse trees *)
diff -r a594429637fd -r fdd6989cc8a0 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ML/ml_env.ML	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Pure/ML/ml_parse.ML
--- a/src/Pure/ML/ml_parse.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ML/ml_parse.ML	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Wed Feb 17 23:06:24 2016 +0100
@@ -102,8 +102,6 @@
 val raw_explode = SML90.explode;
 val implode = SML90.implode;
 
-val io_buffer_size = 4096;
-
 fun quit () = exit 0;
 
 
diff -r a594429637fd -r fdd6989cc8a0 src/Pure/RAW/ROOT_smlnj.ML
--- a/src/Pure/RAW/ROOT_smlnj.ML	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/compiler_polyml.ML
--- a/src/Pure/RAW/compiler_polyml.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/RAW/compiler_polyml.ML	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/ml_name_space.ML
--- a/src/Pure/RAW/ml_name_space.ML	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/ml_system.ML
--- a/src/Pure/RAW/ml_system.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/RAW/ml_system.ML	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/overloading_smlnj.ML
--- a/src/Pure/RAW/overloading_smlnj.ML	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/pp_dummy.ML
--- a/src/Pure/RAW/pp_dummy.ML	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/proper_int.ML
--- a/src/Pure/RAW/proper_int.ML	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/single_assignment.ML
--- a/src/Pure/RAW/single_assignment.ML	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/thread_dummy.ML
--- a/src/Pure/RAW/thread_dummy.ML	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/universal.ML
--- a/src/Pure/RAW/universal.ML	Wed Feb 17 21:08:18 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 a594429637fd -r fdd6989cc8a0 src/Pure/RAW/use_context.ML
--- a/src/Pure/RAW/use_context.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/RAW/use_context.ML	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ROOT	Wed Feb 17 23:06:24 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"
@@ -179,13 +163,10 @@
     "Isar/token.ML"
     "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/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"
diff -r a594429637fd -r fdd6989cc8a0 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Pure/ROOT.ML	Wed Feb 17 23:06:24 2016 +0100
@@ -76,7 +76,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 +98,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_polyml.ML";
 
 if ML_System.name = "polyml-5.5.0"
   orelse ML_System.name = "polyml-5.5.1"
@@ -123,8 +121,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 ()
@@ -203,13 +200,11 @@
 use "ML/ml_syntax.ML";
 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/exn_output_polyml.ML";
 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 "ML/ml_compiler_polyml.ML";
 
 use "skip_proof.ML";
 use "goal.ML";
@@ -359,7 +354,7 @@
 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 a594429637fd -r fdd6989cc8a0 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Tools/Code/code_runtime.ML	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Tools/ROOT
--- a/src/Tools/ROOT	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Tools/ROOT	Wed Feb 17 23:06:24 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 a594429637fd -r fdd6989cc8a0 src/Tools/Spec_Check/spec_check.ML
--- a/src/Tools/Spec_Check/spec_check.ML	Wed Feb 17 21:08:18 2016 +0100
+++ b/src/Tools/Spec_Check/spec_check.ML	Wed Feb 17 23:06:24 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}