# HG changeset patch
# User wenzelm
# Date 1237844282 -3600
# Node ID df6ca2f50199a411bc5d33548885362f7af3c8bd
# Parent  edca392a2abb5a47fcf7d6ff032766019144e1f8
eliminated Output.ml_output;

diff -r edca392a2abb -r df6ca2f50199 src/Pure/ML/ml_test.ML
--- a/src/Pure/ML/ml_test.ML	Mon Mar 23 22:37:41 2009 +0100
+++ b/src/Pure/ML/ml_test.ML	Mon Mar 23 22:38:02 2009 +0100
@@ -27,8 +27,6 @@
 
 fun eval do_run verbose pos toks =
   let
-    val (print, err) = Output.ml_output;
-
     val input = toks |> map (fn tok =>
       (serial (), (String.explode (ML_Lex.text_of tok), ML_Lex.pos_of tok)));
     val index_pos = Inttab.lookup (Inttab.make (map (apsnd snd) input));
@@ -78,8 +76,8 @@
         PolyML.compiler (get, parameters) ())
       handle exn =>
        (put ("Exception- " ^ General.exnMessage exn ^ " raised");
-        err (output ()); raise exn);
-  in if verbose then print (output ()) else () end;
+        error (output ()); raise exn);
+  in if verbose then writeln (output ()) else () end;
 
 
 (* ML test command *)