src/HOL/Tools/Function/function.ML

--- a/src/HOL/Tools/Function/function.ML	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML	Mon Jan 20 21:32:41 2014 +0100
@@ -278,10 +278,7 @@
 (* setup *)
 
 val setup =
-  Attrib.setup @{binding fundef_cong}
-    (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
-    "declaration of congruence rule for function definitions"
-  #> setup_case_cong
+  setup_case_cong
   #> Function_Common.Termination_Simps.setup
 
 val get_congs = Function_Ctx_Tree.get_function_congs