src/Pure/Syntax/syn_ext.ML
changeset 33037 b22e44496dc2
parent 32785 ec5292653aff
child 33038 8f9594c31de4
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -352,7 +352,7 @@
     1.4    in
     1.5      SynExt {
     1.6        xprods = xprods,
     1.7 -      consts = consts union_string mfix_consts,
     1.8 +      consts = gen_union (op =) (consts, mfix_consts),
     1.9        prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
    1.10        parse_ast_translation = parse_ast_translation,
    1.11        parse_rules = parse_rules' @ parse_rules,