src/Pure/Thy/thy_info.ML
changeset 70067 0cb8753bdb50
parent 70064 f8293bf510a0
child 70072 def3ec9cdb7e
     1.1 --- a/src/Pure/Thy/thy_info.ML	Sat Mar 09 13:35:49 2019 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Mar 09 23:57:07 2019 +0100
     1.3 @@ -295,7 +295,7 @@
     1.4        in (results, (st', pos')) end;
     1.5  
     1.6      val (results, (end_state, end_pos)) =
     1.7 -      fold_map element_result elements (Toplevel.init (), Position.none);
     1.8 +      fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
     1.9  
    1.10      val thy = Toplevel.end_theory end_pos end_state;
    1.11    in (results, thy) end;
    1.12 @@ -455,7 +455,7 @@
    1.13        Outer_Syntax.parse thy pos txt
    1.14        |> map (Toplevel.modify_init (K thy));
    1.15      val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
    1.16 -    val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init ());
    1.17 +    val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
    1.18    in Toplevel.end_theory end_pos end_state end;
    1.19  
    1.20