# HG changeset patch
# User ballarin
# Date 1051524105 -7200
# Node ID 0eb3d91b519a47e06a9c0e15b9e3327913477282
# Parent  38d43d168e8782e7ab88707b124e89d08c1eabe4
Simplifier no longer aborts on failed congruence proof.

diff -r 38d43d168e87 -r 0eb3d91b519a src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Apr 28 10:33:57 2003 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Apr 28 12:01:45 2003 +0200
@@ -704,11 +704,11 @@
          is handled when congc is called *)
       val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
       val unit = trace_thm "Applying congruence rule:" thm';
-      fun err (msg, thm) = (prthm false msg thm; error "Failed congruence proof!")
+      fun err (msg, thm) = (trace_thm msg thm; None)
   in case prover thm' of
-       None => err ("Could not prove", thm')
+       None => err ("Congruence proof failed.  Could not prove", thm')
      | Some thm2 => (case check_conv true (beta_eta_conversion t) thm2 of
-          None => err ("Should not have proved", thm2)
+          None => err ("Congruence proof failed.  Should not have proved", thm2)
         | Some thm2' =>
             if op aconv (pairself term_of (dest_equals (cprop_of thm2')))
             then None else Some thm2')