--- a/src/Pure/Thy/thy_info.ML Thu Nov 03 16:08:28 2022 +0100
+++ b/src/Pure/Thy/thy_info.ML Thu Nov 03 20:10:35 2022 +0100
@@ -292,7 +292,7 @@
in (results, (st', pos')) end;
val (results, (end_state, end_pos)) =
- fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
+ fold_map element_result elements (Toplevel.make_state NONE, Position.none);
val thy = Toplevel.end_theory end_pos end_state;
in (results, thy) end;
@@ -434,7 +434,7 @@
let
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 ());
+ val end_state = fold (Toplevel.command_exception true) trs (Toplevel.make_state NONE);
in Toplevel.end_theory end_pos end_state end;