src/Pure/Thy/thy_info.ML
changeset 76415 f362975e8ba1
parent 76405 aaf307f865c9
child 76432 d0079b509d99
--- 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;