1.1 --- a/src/Pure/Syntax/parser.ML	Fri Apr 08 14:20:57 2011 +0200
     1.2 +++ b/src/Pure/Syntax/parser.ML	Fri Apr 08 15:02:11 2011 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  sig
     1.5    type gram
     1.6    val empty_gram: gram
     1.7 -  val extend_gram: Syn_Ext.xprod list -> gram -> gram
     1.8 +  val extend_gram: Syntax_Ext.xprod list -> gram -> gram
     1.9    val merge_gram: gram * gram -> gram
    1.10    val pretty_gram: gram -> Pretty.T list
    1.11    datatype parsetree =
    1.12 @@ -468,10 +468,10 @@
    1.13            delimiters and predefined terms are stored as terminals,
    1.14            nonterminals are converted to integer tags*)
    1.15          fun symb_of [] nt_count tags result = (nt_count, tags, rev result)
    1.16 -          | symb_of (Syn_Ext.Delim s :: ss) nt_count tags result =
    1.17 +          | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result =
    1.18                symb_of ss nt_count tags
    1.19                  (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result)
    1.20 -          | symb_of (Syn_Ext.Argument (s, p) :: ss) nt_count tags result =
    1.21 +          | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result =
    1.22                let
    1.23                  val (nt_count', tags', new_symb) =
    1.24                    (case Lexicon.predef_term s of
    1.25 @@ -485,7 +485,7 @@
    1.26          (*Convert list of productions by invoking symb_of for each of them*)
    1.27          fun prod_of [] nt_count prod_count tags result =
    1.28                (nt_count, prod_count, tags, result)
    1.29 -          | prod_of (Syn_Ext.XProd (lhs, xsymbs, const, pri) :: ps)
    1.30 +          | prod_of (Syntax_Ext.XProd (lhs, xsymbs, const, pri) :: ps)
    1.31                  nt_count prod_count tags result =
    1.32                let
    1.33                  val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs;