src/Pure/Syntax/syn_ext.ML
changeset 11546 2b3f02227c35
parent 9380 63cca60b2cce
child 12513 0ffb824dc95c
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Sat Sep 01 00:20:22 2001 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Sat Sep 01 00:20:44 2001 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4      SynExt {
     1.5        logtypes = logtypes',
     1.6        xprods = xprods,
     1.7 -      consts = consts union mfix_consts,
     1.8 +      consts = consts union_string mfix_consts,
     1.9        prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
    1.10        parse_ast_translation = parse_ast_translation,
    1.11        parse_rules = parse_rules,