src/Pure/ML-Systems/smlnj.ML
changeset 28284 2161665a0a5d
parent 28268 ac8431ecd57e
child 28443 de653f1ad78b
     1.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 17 23:23:49 2008 +0200
     1.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 17 23:44:31 2008 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4    in use_text tune str_of_pos name_space (1, name) output verbose txt end;
     1.5  
     1.6  fun forget_structure name =
     1.7 -  use_text (fn x => x) (fn _ => "") (1, "ML") (TextIO.print, fn s => raise Fail s) false
     1.8 +  use_text (fn x => x) (fn _ => "") () (1, "ML") (TextIO.print, fn s => raise Fail s) false
     1.9      ("structure " ^ name ^ " = struct end");
    1.10  
    1.11