diff -r a9e574e2cba5 -r f8293bf510a0 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Mar 09 10:31:20 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Mar 09 13:19:13 2019 +0100
@@ -295,7 +295,7 @@
       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;
@@ -455,7 +455,7 @@
       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;