tuned signature;

--- a/src/Pure/Syntax/syntax.ML	Sun May 26 20:08:53 2013 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun May 26 20:42:43 2013 +0200
@@ -91,8 +91,6 @@
   val mode_input: mode
   val empty_syntax: syntax
   val merge_syntax: syntax * syntax -> syntax
-  val token_markers: string list
-  val basic_nonterms: string list
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
@@ -528,20 +526,6 @@
   end;
 
 
-(* basic syntax *)
-
-val token_markers =
-  ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
-
-val basic_nonterms =
-  Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
-    "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
-    "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
-    "float_position", "xnum_position", "index", "struct", "tid_position",
-    "tvar_position", "id_position", "longid_position", "var_position", "str_position",
-    "type_name", "class_name"];
-
-
 
 (** print syntax **)
 

--- a/src/Pure/Syntax/syntax_phases.ML	Sun May 26 20:08:53 2013 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun May 26 20:42:43 2013 +0200
@@ -517,7 +517,7 @@
     val {structs, fixes} = idents;
 
     fun mark_atoms ((t as Const (c, _)) $ u) =
-          if member (op =) Syntax.token_markers c
+          if member (op =) Pure_Thy.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)

--- a/src/Pure/pure_thy.ML	Sun May 26 20:08:53 2013 +0200
+++ b/src/Pure/pure_thy.ML	Sun May 26 20:42:43 2013 +0200
@@ -8,6 +8,7 @@
 sig
   val old_appl_syntax: theory -> bool
   val old_appl_syntax_setup: theory -> theory
+  val token_markers: string list
 end;
 
 structure Pure_Thy: PURE_THY =
@@ -52,6 +53,9 @@
 
 (* main content *)
 
+val token_markers =
+  ["_tfree", "_tvar", "_free", "_bound", "_loose", "_var", "_numeral", "_inner_string"];
+
 val _ = Context.>> (Context.map_theory
   (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
    Old_Appl_Syntax.put false #>
@@ -60,8 +64,15 @@
     (Binding.name "prop", 0, NoSyn),
     (Binding.name "itself", 1, NoSyn),
     (Binding.name "dummy", 0, NoSyn)]
-  #> Sign.add_nonterminals_global (map Binding.name Syntax.basic_nonterms)
-  #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
+  #> Sign.add_nonterminals_global
+    (map Binding.name
+      (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
+        "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
+        "any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
+        "float_position", "xnum_position", "index", "struct", "tid_position",
+        "tvar_position", "id_position", "longid_position", "var_position", "str_position",
+        "type_name", "class_name"]))
+  #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) token_markers)
   #> Sign.add_syntax_i
    [("",            typ "prop' => prop",               Delimfix "_"),
     ("",            typ "logic => any",                Delimfix "_"),