diff -r cf58486ca11b -r c33450acd873 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun Jan 21 13:27:41 2007 +0100
+++ b/src/Pure/codegen.ML	Sun Jan 21 16:43:42 2007 +0100
@@ -991,7 +991,7 @@
                   [Pretty.str "]"])]],
             Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
       "\n\nend;\n") ();
-    val _ = use_text Output.ml_output false s;
+    val _ = use_text "" Output.ml_output false s;
     fun iter f k = if k > i then NONE
       else (case (f () handle Match =>
           (warning "Exception Match raised in generated code"; NONE)) of
@@ -1043,7 +1043,7 @@
             [Pretty.str "result"],
           Pretty.str ";"])  ^
       "\n\nend;\n";
-    val _ = use_text Output.ml_output false s
+    val _ = use_text "" Output.ml_output false s
   in !eval_result end);
 
 fun print_evaluated_term s = Toplevel.keep (fn state =>
@@ -1150,7 +1150,7 @@
        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 => use_text Output.ml_output false
+         NONE => use_text "" Output.ml_output false
            (space_implode "\n" (map snd code))
        | SOME fname =>
            if lib then