src/Pure/raw_simplifier.ML
changeset 59058 a78612c67ec0
parent 58950 d07464875dd4
child 59498 50b60f501b05
     1.1 --- a/src/Pure/raw_simplifier.ML	Wed Nov 26 16:55:43 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Wed Nov 26 20:05:34 2014 +0100
     1.3 @@ -342,7 +342,7 @@
     1.4        val rules' = Net.merge eq_rrule (rules1, rules2);
     1.5        val prems' = Thm.merge_thms (prems1, prems2);
     1.6        val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
     1.7 -      val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
     1.8 +      val congs' = merge (Thm.eq_thm_prop o apply2 #2) (congs1, congs2);
     1.9        val weak' = merge (op =) (weak1, weak2);
    1.10        val procs' = Net.merge eq_proc (procs1, procs2);
    1.11        val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
    1.12 @@ -1036,7 +1036,7 @@
    1.13          (case check_conv ctxt true (Drule.beta_eta_conversion t) thm2 of
    1.14            NONE => err ("Congruence proof failed.  Should not have proved", thm2)
    1.15          | SOME thm2' =>
    1.16 -            if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
    1.17 +            if op aconv (apply2 term_of (Thm.dest_equals (cprop_of thm2')))
    1.18              then NONE else SOME thm2'))
    1.19    end;
    1.20