--- a/src/HOL/Tools/recdef_package.ML Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Tools/recdef_package.ML Fri Mar 04 15:07:34 2005 +0100
@@ -91,7 +91,7 @@
val (del, rest) = Library.partition (Library.equal c o fst) congs;
in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
-val add_congs = curry (Library.foldr (uncurry add_cong));
+val add_congs = foldr (uncurry add_cong);
end;
@@ -272,7 +272,7 @@
fun prepare_hints_old thy (ss, thms) =
let val {simps, congs, wfs} = get_global_hints thy
- in (Classical.claset_of thy, ss addsimps simps, map #2 (add_congs thms congs), wfs) end;
+ in (Classical.claset_of thy, ss addsimps simps, map #2 (add_congs congs thms), wfs) end;
val add_recdef_old = gen_add_recdef Tfl.define Attrib.global_attribute prepare_hints_old false;