src/Pure/ML-Systems/smlnj.ML

--- 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 **)