diff -r 5a3bd2b7d0ee -r 4985f4706c6d src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Sep 08 18:00:37 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Sep 08 22:30:29 2010 +0200
@@ -67,7 +67,7 @@
 fun eval verbose pos toks =
   let
     val _ = Secure.secure_mltext ();
-    val {name_space = space, print, error = err, ...} = ML_Env.local_context;
+    val space = ML_Env.name_space;
 
 
     (* input *)
@@ -147,7 +147,7 @@
         NONE => ()
       | SOME parse_tree => report_parse_tree depth space parse_tree);
       (case phase2 of
-        NONE => err "Static Errors"
+        NONE => error "Static Errors"
       | SOME code =>
           apply_result
             ((code
@@ -171,8 +171,8 @@
         PolyML.compiler (get, parameters) ())
       handle exn =>
        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        err (output ()); reraise exn);
-  in if verbose then print (output ()) else () end;
+        error (output ()));
+  in if verbose then writeln (output ()) else () end;
 
 end;