# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1335870964 -3600
# Node ID 51c475ceaf09c16d732ce2be1d2c7c764a5aa5c9
# Parent  31c64dd4c95a3f7a6ab6755c92062ecf4afab0fb# Parent  25c61cc06ae2d27699f7dc031a988f1f963e4cfa
merged

diff -r 25c61cc06ae2 -r 51c475ceaf09 Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Fri Apr 20 18:58:03 2012 +0200
+++ b/Nominal/nominal_function.ML	Tue May 01 12:16:04 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