--- a/src/Pure/ML-Systems/alice.ML Fri Mar 28 22:39:45 2008 +0100
+++ b/src/Pure/ML-Systems/alice.ML Fri Mar 28 22:39:47 2008 +0100
@@ -19,6 +19,8 @@
val ml_system_fix_ints = false;
+fun forget_structure _ = ();
+
fun exit 0 = (OS.Process.exit OS.Process.success): unit
| exit _ = OS.Process.exit OS.Process.failure;
--- a/src/Pure/ML-Systems/mosml.ML Fri Mar 28 22:39:45 2008 +0100
+++ b/src/Pure/ML-Systems/mosml.ML Fri Mar 28 22:39:47 2008 +0100
@@ -24,6 +24,8 @@
val ml_system_fix_ints = false;
+fun forget_structure _ = ();
+
load "Obj";
load "Bool";
load "Int";
--- a/src/Pure/ML-Systems/polyml_common.ML Fri Mar 28 22:39:45 2008 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Fri Mar 28 22:39:47 2008 +0100
@@ -15,6 +15,9 @@
(** ML system and platform related **)
+val forget_structure = PolyML.Compiler.forgetStructure;
+
+
(* Compiler options *)
val ml_system_fix_ints = false;
--- a/src/Pure/ML-Systems/smlnj.ML Fri Mar 28 22:39:45 2008 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Fri Mar 28 22:39:47 2008 +0100
@@ -52,6 +52,7 @@
Control.Print.printLength := dest_int n);
end;
+
(* compiler-independent timing functions *)
fun start_timing () =
@@ -134,6 +135,10 @@
val txt = TextIO.inputAll instream before TextIO.closeIn instream;
in use_text tune (1, name) output verbose txt end;
+fun forget_structure name =
+ use_text (fn x => x) (1, "ML") (TextIO.print, fn s => raise Fail s) false
+ ("structure " ^ name ^ " = struct end");
+
(** interrupts **)