--- 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