--- a/src/HOL/Tools/recdef_package.ML Tue Sep 20 08:20:22 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML Tue Sep 20 08:21:49 2005 +0200
@@ -245,7 +245,7 @@
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 [];