src/Pure/Thy/thy_info.ML
changeset 70072 def3ec9cdb7e
parent 70067 0cb8753bdb50
child 70197 c8e08d8ffb93
     1.1 --- a/src/Pure/Thy/thy_info.ML	Sun Mar 10 15:31:24 2019 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Mar 10 21:12:29 2019 +0100
     1.3 @@ -451,9 +451,7 @@
     1.4  
     1.5  fun script_thy pos txt thy =
     1.6    let
     1.7 -    val trs =
     1.8 -      Outer_Syntax.parse thy pos txt
     1.9 -      |> map (Toplevel.modify_init (K thy));
    1.10 +    val trs = Outer_Syntax.parse_text thy (K thy) pos txt;
    1.11      val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
    1.12      val end_state = fold (Toplevel.command_exception true) trs (Toplevel.init_toplevel ());
    1.13    in Toplevel.end_theory end_pos end_state end;