Changed the simplifier: if the subgoaler proves an unexpected thm, chances
are, it is an instance of the expected thm. Instead of aborting, rewriting
now fails at that point.

--- a/src/Pure/thm.ML	Thu Nov 11 13:18:49 1993 +0100
+++ b/src/Pure/thm.ML	Thu Nov 11 13:21:59 1993 +0100
@@ -884,14 +884,13 @@
 fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
 
 fun check_conv(thm as Thm{sign,hyps,prop,...}, prop0) =
-  let fun err() = (trace_term "Proved wrong thm" sign prop;
-                   error "Check your prover")
+  let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; None)
       val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0)
   in case prop of
        Const("==",_) $ lhs $ rhs =>
          if (lhs = lhs0) orelse
             (lhs aconv (Envir.norm_term (Envir.empty 0) lhs0))
-         then (trace_thm "SUCCEEDED" thm; ((sign,hyps),rhs))
+         then (trace_thm "SUCCEEDED" thm; Some((sign,hyps),rhs))
          else err()
      | _ => err()
   end;
@@ -912,7 +911,7 @@
            else (trace_thm "Trying to rewrite:" thm';
                  case prover mss thm' of
                    None       => (trace_thm "FAILED" thm'; None)
-                 | Some(thm2) => Some(check_conv(thm2,prop')))
+                 | Some(thm2) => check_conv(thm2,prop'))
         end
 
       fun rewl [] = None
@@ -936,10 +935,12 @@
       val thm' = Thm{sign=sign', hyps=hyps union hypst,
                      prop=prop', maxidx=maxidx}
       val unit = trace_thm "Applying congruence rule" thm';
+      fun err() = error("Failed congruence proof!")
 
   in case prover thm' of
-       None => error("Failed congruence proof!")
-     | Some(thm2) => check_conv(thm2,prop')
+       None => err()
+     | Some(thm2) => (case check_conv(thm2,prop') of
+                        None => err() | Some(x) => x)
   end;