src/Pure/PIDE/resources.ML

--- a/src/Pure/PIDE/resources.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -151,7 +151,7 @@
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
         (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
 
-    val toks = Outer_Syntax.scan keywords text_pos text;
+    val toks = Token.explode keywords text_pos text;
     val spans = Outer_Syntax.parse_spans toks;
     val elements = Thy_Syntax.parse_elements keywords spans;