changeset 55394 | d5ebe055b599 |
parent 55343 | 5ebf832b58a1 |
child 55409 | b74248961819 |
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 12 08:35:56 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 12 08:35:56 2014 +0100 @@ -43,7 +43,7 @@ type T = n2m_sugar Typtab.table; val empty = Typtab.empty; val extend = I; - fun merge data : T = Typtab.merge (eq_fst (eq_list eq_fp_sugar)) data; + fun merge data : T = Typtab.merge (K true) data; ); fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) =