--- a/src/HOL/Fun_Def_Base.thy Wed Oct 29 11:41:54 2014 +0100
+++ b/src/HOL/Fun_Def_Base.thy Wed Oct 29 13:42:38 2014 +0100
@@ -11,8 +11,12 @@
ML_file "Tools/Function/function_lib.ML"
named_theorems termination_simp "simplification rules for termination proofs"
ML_file "Tools/Function/function_common.ML"
-ML_file "Tools/Function/context_tree.ML"
-setup Function_Ctx_Tree.setup
+ML_file "Tools/Function/function_context_tree.ML"
+
+attribute_setup fundef_cong =
+ \<open>Attrib.add_del Function_Context_Tree.cong_add Function_Context_Tree.cong_del\<close>
+ "declaration of congruence rule for function definitions"
+
ML_file "Tools/Function/sum_tree.ML"
end