# HG changeset patch
# User wenzelm
# Date 1221687871 -7200
# Node ID 2161665a0a5d8f8cb3936fe0b2e5ceecff5d8236
# Parent  dbe9c820e4d244f73d946fdc3c8d43def32eeb5c
use_text/use_file now depend on explicit ML name space;

diff -r dbe9c820e4d2 -r 2161665a0a5d Admin/isatest/annomaly.ML
--- 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 ]
diff -r dbe9c820e4d2 -r 2161665a0a5d src/Pure/ML-Systems/smlnj.ML
--- 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");