1.1 --- a/src/Pure/meta_simplifier.ML	Sat May 30 11:56:21 2009 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Sat May 30 11:57:36 2009 +0200
     1.3 @@ -158,11 +158,6 @@
     1.4    Thm.eq_thm_prop (thm1, thm2);
     1.5  
     1.6  
     1.7 -(* congruences *)
     1.8 -
     1.9 -val eq_cong = Thm.eq_thm_prop
    1.10 -
    1.11 -
    1.12  (* simplification sets, procedures, and solvers *)
    1.13  
    1.14  (*A simpset contains data required during conversion:
    1.15 @@ -785,7 +780,7 @@
    1.16        val prems' = merge Thm.eq_thm_prop (prems1, prems2);
    1.17        val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
    1.18        val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
    1.19 -      val congs' = merge (eq_cong o pairself #2) (congs1, congs2);
    1.20 +      val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
    1.21        val weak' = merge (op =) (weak1, weak2);
    1.22        val procs' = Net.merge eq_proc (procs1, procs2);
    1.23        val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);