--- a/src/Pure/Isar/outer_syntax.ML Thu Jan 19 21:22:21 2006 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Thu Jan 19 21:22:22 2006 +0100
@@ -272,7 +272,7 @@
else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
end;
-fun run_thy name path = Output.toplevel_errors (fn () =>
+fun run_thy name path =
let
val text = Source.of_list (Library.untabify (explode (File.read path)));
val _ = Present.init_theory name;
@@ -288,7 +288,7 @@
IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
|> Buffer.content
|> Present.theory_output name
- end) ();
+ end;
in