changeset 3165 | 31c64dd4c95a |
parent 3135 | 92b9b8d2888d |
child 3190 | 1b7c034c9e9e |
--- a/Nominal/nominal_function.ML Thu Apr 19 15:39:46 2012 +0100 +++ b/Nominal/nominal_function.ML Mon Apr 30 15:45:23 2012 +0100 @@ -245,7 +245,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