use_text/use_file now depend on explicit ML name space;

--- a/Admin/isatest/annomaly.ML	Wed Sep 17 23:23:49 2008 +0200
+++ b/Admin/isatest/annomaly.ML	Wed Sep 17 23:44:31 2008 +0200
@@ -44,7 +44,7 @@
 
 in
 
-  fun use_text tune str_of_pos (line, name) p v t =
+  fun use_text tune str_of_pos name_space (line, name) p v t =
     let val name = case name of "" => "unnamed" | name => name
         val arcs = rewrite ["use_text"] name
         (* should we have different files for different line numbers? *
@@ -55,12 +55,12 @@
 		      andalso name = "ML"
 		   then ["empty_Isabelle", "empty" ] else arcs
         val _    = AnnoMaLy.nameNextStream arcs
-    in  smlnj_use_text tune str_of_pos (line, name) p v t  end;
+    in  smlnj_use_text tune str_of_pos name_space (line, name) p v t  end;
 
-  fun use_file tune str_of_pos output verbose name =
+  fun use_file tune str_of_pos name_space output verbose name =
       let val arcs = rewrite ["use_file"] name
           val _    = AnnoMaLy.nameNextStream arcs
-      in  smlnj_use_file tune str_of_pos output verbose name  end;
+      in  smlnj_use_file tune str_of_pos name_space output verbose name  end;
 
   fun forget_structure name =
       let val arcs = [ "forget_structure", name ]

--- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 17 23:23:49 2008 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 17 23:44:31 2008 +0200
@@ -138,7 +138,7 @@
   in use_text tune str_of_pos name_space (1, name) output verbose txt end;
 
 fun forget_structure name =
-  use_text (fn x => x) (fn _ => "") (1, "ML") (TextIO.print, fn s => raise Fail s) false
+  use_text (fn x => x) (fn _ => "") () (1, "ML") (TextIO.print, fn s => raise Fail s) false
     ("structure " ^ name ^ " = struct end");