# HG changeset patch
# User wenzelm
# Date 1163197324 -3600
# Node ID 2b60e9b70a8cca5e926ae13ce69baa9649e883a0
# Parent  3c245a8a500138f8613e07aef536368ab2a7ac06
removed obsolete ML compatibility fragments;

diff -r 3c245a8a5001 -r 2b60e9b70a8c src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Nov 10 23:22:03 2006 +0100
+++ b/src/Pure/IsaMakefile	Fri Nov 10 23:22:04 2006 +0100
@@ -42,13 +42,9 @@
   Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML 		\
   Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML Isar/specification.ML	\
   Isar/term_style.ML Isar/theory_target.ML Isar/thy_header.ML Isar/toplevel.ML	\
-  ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML			\
   ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML			\
   ML-Systems/polyml-4.9.1.ML ML-Systems/polyml-interrupt-timeout.ML		\
   ML-Systems/polyml-posix.ML ML-Systems/polyml.ML ML-Systems/poplogml.ML	\
-  ML-Systems/smlnj-basis-compat.ML ML-Systems/smlnj-compiler.ML			\
-  ML-Systems/smlnj-interrupt-timeout.ML ML-Systems/smlnj-pp-new.ML		\
-  ML-Systems/smlnj-pp-old.ML ML-Systems/smlnj-ptreql.ML				\
   ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML		\
   Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML		\
   Pure.thy ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML		\
diff -r 3c245a8a5001 -r 2b60e9b70a8c src/Pure/ML-Systems/cpu-timer-basis.ML
--- a/src/Pure/ML-Systems/cpu-timer-basis.ML	Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(*  Title:      Pure/ML-Systems/cpu-timer-basis.ML
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
-
-Implementation of timing functions, building on standard ("basis library") functions.
-*)
-
-(*Note start point for timing*)
-fun startTiming() =
-  let val CPUtimer = Timer.startCPUTimer();
-      val time = Timer.checkCPUTimer(CPUtimer)
-  in  (CPUtimer,time)  end;
-
-(*Finish timing and return string*)
-fun endTiming (CPUtimer, {sys,usr}) =
-  let open Time  (*...for Time.toString, Time.+ and Time.- *)
-      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
-  in  "User " ^ toString (usr2-usr) ^
-      "  All "^ toString (sys2-sys + usr2-usr) ^
-      " secs"
-      handle Time => ""
-  end;
-
-fun checkTimer timer =
-  let
-    val {sys, usr} = Timer.checkCPUTimer timer;
-    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
-  in (sys, usr, gc) end;
diff -r 3c245a8a5001 -r 2b60e9b70a8c src/Pure/ML-Systems/cpu-timer-gc.ML
--- a/src/Pure/ML-Systems/cpu-timer-gc.ML	Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(*  Title:      Pure/ML-Systems/cpu-timer-gc.ML
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
-
-Implementation of timing functions, building on implementations where
-the return type of Timer.checkCPUTimer includes a gc field.
-*)
-
-(*Note start point for timing*)
-fun startTiming() =
-  let val CPUtimer = Timer.startCPUTimer();
-      val time = Timer.checkCPUTimer(CPUtimer)
-  in  (CPUtimer,time)  end;
-
-(*Finish timing and return string*)
-fun endTiming (CPUtimer, {gc,sys,usr}) =
-  let open Time  (*...for Time.toString, Time.+ and Time.- *)
-      val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
-  in  "User " ^ toString (usr2-usr) ^
-      "  GC " ^ toString (gc2-gc) ^
-      "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
-      " secs"
-      handle Time => ""
-  end;
-
-fun checkTimer timer =
-  let val {sys, usr, gc} = Timer.checkCPUTimer timer
-  in (sys, usr, gc) end;
diff -r 3c245a8a5001 -r 2b60e9b70a8c src/Pure/ML-Systems/smlnj-basis-compat.ML
--- a/src/Pure/ML-Systems/smlnj-basis-compat.ML	Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      Pure/ML-Systems/smlnj-basis-compat.ML
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
-
-Compatibility file for Standard ML of New Jersey 110.44 or later. Here
-signatures that have changed to adhere to the SML Basis Library are
-changed back to their old values.
-*)
-
-structure TextIO =
-struct
-  open TextIO;
-
-  fun inputLine is =
-    (case TextIO.inputLine is of
-      SOME str => str
-    | NONE => "")
-    handle IO.Io _ => raise Interrupt;
-end;
diff -r 3c245a8a5001 -r 2b60e9b70a8c src/Pure/ML-Systems/smlnj-compiler.ML
--- a/src/Pure/ML-Systems/smlnj-compiler.ML	Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(*  Title:      Pure/ML-Systems/smlnj.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, LMU Muenchen
-
-Compatibility tweak for later versions of Standard ML of New Jersey 110.
-*)
-
-structure Compiler =
-struct
-  open Compiler;
-  structure Control = Control;
-  structure PrettyPrint = PrettyPrint;
-  structure PPTable = CompilerPPTable;
-  structure Interact = Backend.Interact;
-end;
diff -r 3c245a8a5001 -r 2b60e9b70a8c src/Pure/ML-Systems/smlnj-interrupt-timeout.ML
--- a/src/Pure/ML-Systems/smlnj-interrupt-timeout.ML	Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  Title:      Pure/ML-Systems/smlnj-interrupt-timeout.ML
-    ID:         $Id$
-    Author:     Tjark Weber, Makarius
-    Copyright   2006
-
-Bounded time execution (similar to SML/NJ's TimeLimit structure).
-*)
-
-fun interrupt_timeout time f x =
-  TimeLimit.timeLimit time f x
-    handle TimeLimit.TimeOut => raise Interrupt;
diff -r 3c245a8a5001 -r 2b60e9b70a8c src/Pure/ML-Systems/smlnj-pp-new.ML
--- a/src/Pure/ML-Systems/smlnj-pp-new.ML	Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*  Title:      Pure/ML-Systems/smlnj-pp-new.ML
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
-
-Installation of the pretty printer, using SML/NJ's new pretty printer
-interface.
-*)
-
-fun make_pp path pprint =
-  let
-    open Compiler.PrettyPrint;
-
-    fun pp pps obj =
-      pprint obj
-        (string pps, openHOVBox pps o Rel,
-          fn wd => break pps {nsp=wd, offset=0}, fn () => newline pps,
-          fn () => closeBox pps);
-  in
-    (path, pp)
-  end;
diff -r 3c245a8a5001 -r 2b60e9b70a8c src/Pure/ML-Systems/smlnj-pp-old.ML
--- a/src/Pure/ML-Systems/smlnj-pp-old.ML	Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*  Title:      Pure/ML-Systems/smlnj-pp-old.ML
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
-
-Installation of the pretty printer, using SML/NJ's old pretty printer
-interface.
-*)
-
-fun make_pp path pprint =
-  let
-    open Compiler.PrettyPrint;
-
-    fun pp pps obj =
-      pprint obj
-        (add_string pps, begin_block pps INCONSISTENT,
-          fn wd => add_break pps (wd, 0), fn () => add_newline pps,
-          fn () => end_block pps);
-  in
-    (path, pp)
-  end;
diff -r 3c245a8a5001 -r 2b60e9b70a8c src/Pure/ML-Systems/smlnj-ptreql.ML
--- a/src/Pure/ML-Systems/smlnj-ptreql.ML	Fri Nov 10 23:22:03 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,10 +0,0 @@
-(*  Title:      $Id$
-    Author:     Lawrence C Paulson
-
-Pointer Equality: for Standard ML of New Jersey 110.49 or later.
-
-Thanks to Matthias Blume for providing InlineT.ptreql!
-*)
-
-CM.autoload "$smlnj/init/init.cmi";
-val pointer_eq = InlineT.ptreql;