diff -r c68c1b89a0f1 -r fcc4b89a600d src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Feb 24 14:14:07 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Sun Feb 24 17:29:55 2013 +0100
@@ -268,9 +268,8 @@
       val id_string = print_id id;
       val span = Lazy.lazy (fn () =>
         Position.setmp_thread_data (Position.id_only id_string)
-          (fn () =>
-            Thy_Syntax.parse_tokens
-              (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
+          (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
+            ());
       val _ =
         Position.setmp_thread_data (Position.id_only id_string)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
@@ -453,7 +452,7 @@
           (fn () =>
             let
               val tr =
-                #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
+                Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
                 |> modify_init
                 |> Toplevel.put_id exec_id'_string;
               val cmts = Outer_Syntax.span_cmts span;