--- a/src/HOL/Tools/function_package/fundef_package.ML Thu May 11 19:15:16 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Thu May 11 19:19:31 2006 +0200
@@ -162,8 +162,8 @@
(* congruence rules *)
-val cong_add = Thm.declaration_attribute (map_fundef_congs o cons o safe_mk_meta_eq);
-val cong_del = Thm.declaration_attribute (map_fundef_congs o remove (op =) o safe_mk_meta_eq);
+val cong_add = Thm.declaration_attribute (map_fundef_congs o Drule.add_rule o safe_mk_meta_eq);
+val cong_del = Thm.declaration_attribute (map_fundef_congs o Drule.del_rule o safe_mk_meta_eq);
(* setup *)