src/HOL/Tools/recdef_package.ML

       is simplified. Many induction rules have nested implications that would
       give rise to looping conditional rewriting.*)
     val (thy, {rules = rules_idx, induct, tcs}) =
         tfl_fn strict thy cs (ss delcongs [imp_cong])
                congs wfs name R eqs;
-    val rules = map (map #1) (Library.partition_eq Library.eq_snd rules_idx);
+    val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
     val simp_att = if null tcs then
       [Simplifier.simp_add_global, RecfunCodegen.add NONE] else [];
 
     val (thy, (simps' :: rules', [induct'])) =
       thy