# HG changeset patch
# User nipkow
# Date 826569775 -3600
# Node ID a89f246dee0eef01e94044e3ae2c6415b4dd0e5b
# Parent  630d881b51bdcfa77f7c8b1eab5bb6686c23b4f9
Non-matching congruence rule in rewriter is simply ignored.
Used to cause error message.

diff -r 630d881b51bd -r a89f246dee0e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Mar 11 14:19:12 1996 +0100
+++ b/src/Pure/thm.ML	Mon Mar 11 19:42:55 1996 +0100
@@ -1599,8 +1599,9 @@
                   else Logic.incr_indexes([],maxidxt+1) prop;
       val rlhs = if maxidxt = ~1 then lhs
                  else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
-      val insts = Pattern.match tsig (rlhs,t) handle Pattern.MATCH =>
-                  error("Congruence rule did not match")
+      val insts = Pattern.match tsig (rlhs,t)
+      (* Pattern.match can raise Pattern.MATCH;
+         is handled when congc is called *)
       val prop' = ren_inst(insts,rprop,rlhs,t);
       val shyps' = add_insts_sorts (insts, shyps union shypst)
       val maxidx' = maxidx_of_term prop'
@@ -1687,7 +1688,8 @@
 		    Const(a,_) =>
 		      (case assoc(congs,a) of
 			 None => appc()
-		       | Some(cong) => congc (prover mss,sign) cong trec)
+		       | Some(cong) => (congc (prover mss,sign) cong trec
+                                        handle Pattern.MATCH => appc() ) )
 		  | _ => appc()
 	       end)
 	 | _ => None)