Nominal/nominal_function.ML
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