src/Pure/codegen.ML

--- a/src/Pure/codegen.ML	Mon Mar 24 18:44:21 2008 +0100
+++ b/src/Pure/codegen.ML	Mon Mar 24 23:34:24 2008 +0100
@@ -963,7 +963,7 @@
                   [Pretty.str "]"])]]),
           Pretty.str ");"]) ^
       "\n\nend;\n") ();
-    val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy));
+    val _ = ML_Context.use_mltext false Position.none s (SOME (Context.Theory thy));
     fun iter f k = if k > i then NONE
       else (case (f () handle Match =>
           (if quiet then ()
@@ -1053,7 +1053,7 @@
               [Pretty.str "(result ())"],
             Pretty.str ");"]) ^
         "\n\nend;\n";
-      val _ = ML_Context.use_mltext s false (SOME (Context.Theory thy))
+      val _ = ML_Context.use_mltext false Position.none s (SOME (Context.Theory thy));
     in !eval_result end) ();
   in e () end;
 
@@ -1148,8 +1148,8 @@
        val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
        val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
      in ((case opt_fname of
-         NONE => ML_Context.use_mltext (space_implode "\n" (map snd code))
-           false (SOME (Context.Theory thy))
+         NONE => ML_Context.use_mltext false Position.none (space_implode "\n" (map snd code))
+           (SOME (Context.Theory thy))
        | SOME fname =>
            if lib then
              app (fn (name, s) => File.write