src/Pure/Thy/thy_info.ML

         val (results, st') = Toplevel.element_result keywords elem st;
         val pos' = Toplevel.pos_of (Thy_Element.last_element elem);
       in (results, (st', pos')) end;
 
     val (results, (end_state, end_pos)) =
-      fold_map element_result elements (Toplevel.toplevel, Position.none);
+      fold_map element_result elements (Toplevel.init (), Position.none);
 
     val thy = Toplevel.end_theory end_pos end_state;
   in (results, thy) end;
 
 fun eval_thy (context: context) update_time master_dir header text_pos text parents =

   let
     val trs =
       Outer_Syntax.parse thy pos txt
       |> map (Toplevel.modify_init (K thy));
     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.toplevel;
+    val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init ());
   in Toplevel.end_theory end_pos end_state end;
 
 
 (* register theory *)