# HG changeset patch
# User wenzelm
# Date 1028575065 -7200
# Node ID a73823f70159b689025001b592c4ba418011efe1
# Parent  7ddcf40a80b3384419058d9178cd1d79e88de1b1
protect simplifier operation against spurious exceptions from simprocs;

diff -r 7ddcf40a80b3 -r a73823f70159 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Aug 05 21:17:04 2002 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Aug 05 21:17:45 2002 +0200
@@ -651,9 +651,10 @@
       | proc_rews ({name, proc, lhs, ...} :: ps) =
           if Pattern.matches tsigt (term_of lhs, term_of t) then
             (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
-             case proc signt prems eta_t of
-               None => (debug false "FAILED"; proc_rews ps)
-             | Some raw_thm =>
+             case try (fn () => proc signt prems eta_t) () of
+               None => (debug true "EXCEPTION in simproc"; proc_rews ps)
+             | Some None => (debug false "FAILED"; proc_rews ps)
+             | Some (Some raw_thm) =>
                  (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
                   (case rews (mk_procrule raw_thm) of
                     None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps)