src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Sun Nov 25 18:50:13 2012 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sun Nov 25 19:49:24 2012 +0100
@@ -167,7 +167,7 @@
 (* outer syntax token -- with optional YXML content *)
 
 fun token_position (XML.Elem ((name, props), _)) =
-      if name = Isabelle_Markup.tokenN then Position.of_properties props
+      if name = Markup.tokenN then Position.of_properties props
       else Position.none
   | token_position (XML.Text _) = Position.none;
 
@@ -190,7 +190,7 @@
   in
     (case YXML.parse_body str handle Fail msg => error msg of
       body as [tree as XML.Elem ((name, _), _)] =>
-        if name = Isabelle_Markup.tokenN then parse_tree tree else decode body
+        if name = Markup.tokenN then parse_tree tree else decode body
     | [tree as XML.Text _] => parse_tree tree
     | body => decode body)
   end;