--- a/src/HOL/Tools/recdef_package.ML Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML Fri May 05 17:17:21 2006 +0200
@@ -30,7 +30,7 @@
val recdef_tc_i: bstring * attribute list -> string -> int option -> theory -> Proof.state
val setup: theory -> theory
-(* HACK: This has to be exported, since the new recdef-package uses the same hints *)
+(* HACK: This has to be exported, since the new fundef-package uses the same hints *)
val get_local_hints: ProofContext.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
val get_global_hints: theory -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
end;
@@ -300,7 +300,7 @@
LocalRecdefData.init #>
Attrib.add_attributes
[(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
- (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
+ (recdef_congN, Attrib.add_del_args (FundefPackage.cong_add o cong_add) (FundefPackage.cong_del o cong_del), "declaration of recdef cong rule"),
(recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];