# HG changeset patch
# User berghofe
# Date 1005558295 -3600
# Node ID 13c5469b4bb38764423e595178f79823c9353912
# Parent  3a7fe282af9dfb8c297d60263f94cbb6b119c0dd
congc now returns None if congruence rule has no effect.

diff -r 3a7fe282af9d -r 13c5469b4bb3 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Nov 12 10:43:25 2001 +0100
+++ b/src/Pure/meta_simplifier.ML	Mon Nov 12 10:44:55 2001 +0100
@@ -653,7 +653,7 @@
           else proc_rews ps;
   in case eta_t of
        Abs _ $ _ => Some (transitive eta_thm
-         (beta_conversion false (rhs_of eta_thm)), skel0)
+         (beta_conversion false eta_t'), skel0)
      | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of
                None => proc_rews (Net.match_term procs eta_t)
              | some => some)
@@ -678,7 +678,9 @@
        None => err ("Could not prove", thm')
      | Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
           None => err ("Should not have proved", thm2)
-        | Some thm2' => thm2')
+        | Some thm2' =>
+            if op aconv (pairself term_of (dest_equals (cprop_of thm2')))
+            then None else Some thm2')
   end;
 
 val (cA, (cB, cC)) =
@@ -687,6 +689,9 @@
 fun transitive' thm1 None = Some thm1
   | transitive' thm1 (Some thm2) = Some (transitive thm1 thm2);
 
+fun transitive'' None thm2 = Some thm2
+  | transitive'' (Some thm1) thm2 = Some (transitive thm1 thm2);
+
 fun bottomc ((simprem,useprem,mutsimp), prover, sign, maxidx) =
   let
     fun botc skel mss t =
@@ -759,15 +764,15 @@
    may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)
                           (let
                              val thm = congc (prover mss, sign, maxidx) cong t0;
-                             val t = rhs_of thm;
+                             val t = if_none (apsome rhs_of thm) t0;
                              val (cl, cr) = Thm.dest_comb t
                              val dVar = Var(("", 0), dummyT)
                              val skel =
                                list_comb (h, replicate (length ts) dVar)
                            in case botc skel mss cl of
-                                None => Some thm
-                              | Some thm' => Some (transitive thm
-                                  (combination thm' (reflexive cr)))
+                                None => thm
+                              | Some thm' => transitive'' thm
+                                  (combination thm' (reflexive cr))
                            end handle TERM _ => error "congc result"
                                     | Pattern.MATCH => appc ()))
                   | _ => appc ()