src/Pure/Thy/thy_info.ML

--- a/src/Pure/Thy/thy_info.ML	Fri Nov 07 16:22:25 2014 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Nov 07 16:36:55 2014 +0100
@@ -373,7 +373,7 @@
 fun script_thy pos txt thy =
   let
     val trs =
-      Outer_Syntax.parse (Outer_Syntax.get_syntax ()) pos txt
+      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;