diff -r 0398a5e802d3 -r 85eceef2edc7 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 18 07:36:38 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Sep 18 07:46:00 2007 +0200
@@ -26,7 +26,6 @@
     val setup_termination_proof : string option -> local_theory -> Proof.state
 
     val setup : theory -> theory
-    val setup_case_cong_hook : theory -> theory
     val get_congs : theory -> thm list
 end
 
@@ -176,11 +175,10 @@
                            |> safe_mk_meta_eq)))
                        thy
 
-val case_cong_hook = fold add_case_cong
+val case_cong = fold add_case_cong
 
-val setup_case_cong_hook =
-    DatatypeHooks.add case_cong_hook
-    #> (fn thy => case_cong_hook (Symtab.keys (DatatypePackage.get_datatypes thy)) thy)
+val setup_case_cong = DatatypePackage.add_interpretator case_cong
+
 
 
 (* ad-hoc method to convert elimination-style goals to existential statements *)
@@ -259,7 +257,7 @@
   Attrib.add_attributes
     [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del,
       "declaration of congruence rule for function definitions")]
-  #> setup_case_cong_hook
+  #> setup_case_cong
   #> FundefRelation.setup
   #> elim_to_cases_setup