src/Pure/ML-Systems/smlnj.ML
changeset 26474 94735cff132c
parent 26385 ae7564661e76
child 26504 6e87c0a60104
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Fri Mar 28 22:39:45 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Fri Mar 28 22:39:47 2008 +0100
     1.3 @@ -52,6 +52,7 @@
     1.4      Control.Print.printLength := dest_int n);
     1.5  end;
     1.6  
     1.7 +
     1.8  (* compiler-independent timing functions *)
     1.9  
    1.10  fun start_timing () =
    1.11 @@ -134,6 +135,10 @@
    1.12      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.13    in use_text tune (1, name) output verbose txt end;
    1.14  
    1.15 +fun forget_structure name =
    1.16 +  use_text (fn x => x) (1, "ML") (TextIO.print, fn s => raise Fail s) false
    1.17 +    ("structure " ^ name ^ " = struct end");
    1.18 +
    1.19  
    1.20  
    1.21  (** interrupts **)