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,