# HG changeset patch
# User wenzelm
# Date 1206740387 -3600
# Node ID 94735cff132c8066b5af9621795b5a6df8773144
# Parent  2266e5fd7b632d68ef839a63ea795f1a8a1932ce
added forget_structure;

diff -r 2266e5fd7b63 -r 94735cff132c src/Pure/ML-Systems/alice.ML
--- 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;
 
diff -r 2266e5fd7b63 -r 94735cff132c src/Pure/ML-Systems/mosml.ML
--- 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";
diff -r 2266e5fd7b63 -r 94735cff132c src/Pure/ML-Systems/polyml_common.ML
--- 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;
diff -r 2266e5fd7b63 -r 94735cff132c 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 **)