src/Pure/meta_simplifier.ML
changeset 13458 a73823f70159
parent 13196 08c42252346f
child 13486 54464ea94d6f
     1.1 --- a/src/Pure/meta_simplifier.ML	Mon Aug 05 21:17:04 2002 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Aug 05 21:17:45 2002 +0200
     1.3 @@ -651,9 +651,10 @@
     1.4        | proc_rews ({name, proc, lhs, ...} :: ps) =
     1.5            if Pattern.matches tsigt (term_of lhs, term_of t) then
     1.6              (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
     1.7 -             case proc signt prems eta_t of
     1.8 -               None => (debug false "FAILED"; proc_rews ps)
     1.9 -             | Some raw_thm =>
    1.10 +             case try (fn () => proc signt prems eta_t) () of
    1.11 +               None => (debug true "EXCEPTION in simproc"; proc_rews ps)
    1.12 +             | Some None => (debug false "FAILED"; proc_rews ps)
    1.13 +             | Some (Some raw_thm) =>
    1.14                   (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
    1.15                    (case rews (mk_procrule raw_thm) of
    1.16                      None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps)