removed obsolete Output.ML_errors/toplevel_errors;
authorwenzelm
Sun, 29 Jul 2007 16:00:05 +0200
changeset 24056 e134e757fc64
parent 24055 f7483532537b
child 24057 f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
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