src/Pure/PIDE/document.ML
changeset 58903 38c72f5f6c2e
parent 57918 f5d73caba4e5
child 58918 8d36bc5eaed3
--- a/src/Pure/PIDE/document.ML	Wed Nov 05 20:05:32 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Nov 05 20:20:57 2014 +0100
@@ -318,7 +318,7 @@
       val span =
         Lazy.lazy (fn () =>
           Position.setmp_thread_data (Position.id_only id)
-            (fn () => Outer_Syntax.scan (Keyword.get_lexicons ()) (Position.id id) text) ());
+            (fn () => Outer_Syntax.scan (Keyword.get_keywords ()) (Position.id id) text) ());
       val _ =
         Position.setmp_thread_data (Position.id_only id)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();