src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55394 d5ebe055b599
parent 55067 a452de24a877
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -97,12 +97,12 @@
     1.4      val pre_bnfss = map #pre_bnfs fp_sugars;
     1.5      val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
     1.6      val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
     1.7 -    val fp_nesty_bnfs = distinct eq_bnf (flat fp_nesty_bnfss);
     1.8 +    val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
     1.9  
    1.10      val rels =
    1.11        let
    1.12          fun find_rel T As Bs = fp_nesty_bnfss
    1.13 -          |> map (filter_out (curry eq_bnf BNF_Comp.DEADID_bnf))
    1.14 +          |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
    1.15            |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
    1.16            |> Option.map (fn bnf =>
    1.17              let val live = live_of_bnf bnf;