src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
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)) =