diff -r 2065f49da190 -r 2ed2eaabe3df src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Wed Oct 29 17:01:44 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML	Wed Oct 29 19:01:49 2014 +0100
@@ -32,7 +32,6 @@
   val termination : term option -> local_theory -> Proof.state
   val termination_cmd : string option -> local_theory -> Proof.state
 
-  val setup : theory -> theory
   val get_congs : Proof.context -> thm list
 
   val get_info : Proof.context -> term -> info
@@ -264,7 +263,6 @@
 
 (* Datatype hook to declare datatype congs as "function_congs" *)
 
-
 fun add_case_cong n thy =
   let
     val cong = #case_cong (Old_Datatype_Data.the_info thy n)
@@ -274,12 +272,10 @@
       (Function_Context_Tree.map_function_congs (Thm.add_thm cong)) thy
   end
 
-val setup_case_cong = Old_Datatype_Data.interpretation (K (fold add_case_cong))
+val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_case_cong)))
 
 
-(* setup *)
-
-val setup = setup_case_cong
+(* get info *)
 
 val get_congs = Function_Context_Tree.get_function_congs