# HG changeset patch
# User wenzelm
# Date 1185717605 -7200
# Node ID e134e757fc64626eff4f6d0d2c10f049c9435454
# Parent  f7483532537bbf38998214f37683c80b2da067bc
removed obsolete Output.ML_errors/toplevel_errors;

diff -r f7483532537b -r e134e757fc64 src/Pure/Thy/ml_context.ML
--- a/src/Pure/Thy/ml_context.ML	Sun Jul 29 16:00:04 2007 +0200
+++ b/src/Pure/Thy/ml_context.ML	Sun Jul 29 16:00:05 2007 +0200
@@ -161,8 +161,7 @@
       |> #1 |> split_list |> pairself implode;
   in (isabelle_struct decls, body) end);
 
-fun eval name verbose txt =
-  Output.ML_errors (use_text name Output.ml_output verbose) txt;
+fun eval name verbose txt = use_text name Output.ml_output verbose txt;
 
 in