changeset 47701 | 157e6108a342 |
parent 46961 | 5c6955f487e5 |
child 48995 | 0e1cab4a334e |
--- a/src/HOL/Tools/Function/function.ML Mon Apr 23 18:42:05 2012 +0200 +++ b/src/HOL/Tools/Function/function.ML Mon Apr 23 21:44:36 2012 +0200 @@ -265,7 +265,6 @@ (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del) "declaration of congruence rule for function definitions" #> setup_case_cong - #> Function_Relation.setup #> Function_Common.Termination_Simps.setup val get_congs = Function_Ctx_Tree.get_function_congs