removed obsolete Output.ML_errors/toplevel_errors;
authorwenzelm
Sun Jul 29 16:00:05 2007 +0200 (2007-07-29)
changeset 24056e134e757fc64
parent 24055 f7483532537b
child 24057 f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
src/Pure/Thy/ml_context.ML
     1.1 --- a/src/Pure/Thy/ml_context.ML	Sun Jul 29 16:00:04 2007 +0200
     1.2 +++ b/src/Pure/Thy/ml_context.ML	Sun Jul 29 16:00:05 2007 +0200
     1.3 @@ -161,8 +161,7 @@
     1.4        |> #1 |> split_list |> pairself implode;
     1.5    in (isabelle_struct decls, body) end);
     1.6  
     1.7 -fun eval name verbose txt =
     1.8 -  Output.ML_errors (use_text name Output.ml_output verbose) txt;
     1.9 +fun eval name verbose txt = use_text name Output.ml_output verbose txt;
    1.10  
    1.11  in
    1.12