--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Feb 12 08:35:56 2014 +0100
@@ -97,12 +97,12 @@
val pre_bnfss = map #pre_bnfs fp_sugars;
val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
- val fp_nesty_bnfs = distinct eq_bnf (flat fp_nesty_bnfss);
+ val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
val rels =
let
fun find_rel T As Bs = fp_nesty_bnfss
- |> map (filter_out (curry eq_bnf BNF_Comp.DEADID_bnf))
+ |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
|> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
|> Option.map (fn bnf =>
let val live = live_of_bnf bnf;