--- a/src/Pure/Thy/thy_info.ML Sun Mar 10 15:31:24 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML Sun Mar 10 21:12:29 2019 +0100
@@ -451,9 +451,7 @@
fun script_thy pos txt thy =
let
- val trs =
- Outer_Syntax.parse thy pos txt
- |> map (Toplevel.modify_init (K thy));
+ val trs = Outer_Syntax.parse_text thy (K thy) pos txt;
val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
in Toplevel.end_theory end_pos end_state end;