diff -r 01e83ffa6c54 -r c359896d0f48 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat Sep 15 19:27:35 2007 +0200
+++ b/src/Pure/codegen.ML	Sat Sep 15 19:27:40 2007 +0200
@@ -1031,9 +1031,9 @@
     val t = eval_term thy (Syntax.read_term ctxt s);
     val T = Term.type_of t;
   in
-    writeln (Pretty.string_of
+    Pretty.writeln
       (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]))
+        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
   end);
 
 exception Evaluation of term;