src/Pure/Syntax/syn_ext.ML
changeset 18977 f24c416a4814
parent 18857 c4b4fbd74ffb
child 19004 a72c7a1eb129
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Feb 08 09:27:20 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Feb 08 14:39:00 2006 +0100
     1.3 @@ -166,7 +166,7 @@
     1.4      fun dels_of (XProd (_, xsymbs, _, _)) =
     1.5        List.mapPartial del_of xsymbs;
     1.6    in
     1.7 -    map Symbol.explode (distinct (List.concat (map dels_of xprods)))
     1.8 +    map Symbol.explode (gen_distinct (op =) (List.concat (map dels_of xprods)))
     1.9    end;
    1.10  
    1.11  
    1.12 @@ -362,12 +362,12 @@
    1.13  
    1.14      val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
    1.15        |> split_list |> apsnd (rev o List.concat);
    1.16 -    val mfix_consts = distinct (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
    1.17 +    val mfix_consts = gen_distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
    1.18    in
    1.19      SynExt {
    1.20        xprods = xprods,
    1.21        consts = consts union_string mfix_consts,
    1.22 -      prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
    1.23 +      prmodes = gen_distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
    1.24        parse_ast_translation = parse_ast_translation,
    1.25        parse_rules = parse_rules' @ parse_rules,
    1.26        parse_translation = parse_translation,