diff -r d98eb048a2e4 -r 2074b31650e6 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 14:20:57 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 15:02:11 2011 +0200
@@ -330,7 +330,7 @@
     val (markup, kind, root, constrain) =
       if is_prop
       then (Markup.prop, "proposition", "prop", Type.constraint propT)
-      else (Markup.term, "term", Config.get ctxt Syntax.default_root, I);
+      else (Markup.term, "term", Config.get ctxt Syntax.root, I);
     val (syms, pos) = Syntax.parse_token ctxt markup text;
   in
     let
@@ -491,7 +491,7 @@
     val {structs, fixes} = idents;
 
     fun mark_atoms ((t as Const (c, _)) $ u) =
-          if member (op =) Syntax.token_markers c
+          if member (op =) Syntax_Ext.token_markers c
           then t $ u else mark_atoms t $ mark_atoms u
       | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
       | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
@@ -507,7 +507,7 @@
             else Lexicon.const "_free" $ t
           end
       | mark_atoms (t as Var (xi, T)) =
-          if xi = Syntax.dddot_indexname then Const ("_DDDOT", T)
+          if xi = Syntax_Ext.dddot_indexname then Const ("_DDDOT", T)
           else Lexicon.const "_var" $ t
       | mark_atoms a = a;