src/Pure/meta_simplifier.ML
changeset 13486 54464ea94d6f
parent 13458 a73823f70159
child 13569 69a6b3aa0f38
     1.1 --- a/src/Pure/meta_simplifier.ML	Thu Aug 08 23:50:23 2002 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Thu Aug 08 23:51:24 2002 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  sig
     1.5    include BASIC_META_SIMPLIFIER
     1.6    exception SIMPLIFIER of string * thm
     1.7 +  exception SIMPROC_FAIL of string * exn
     1.8    type meta_simpset
     1.9    val dest_mss          : meta_simpset ->
    1.10      {simps: thm list, congs: thm list, procs: (string * cterm list) list}
    1.11 @@ -63,6 +64,7 @@
    1.12  (** diagnostics **)
    1.13  
    1.14  exception SIMPLIFIER of string * thm;
    1.15 +exception SIMPROC_FAIL of string * exn;
    1.16  
    1.17  val simp_depth = ref 0;
    1.18  
    1.19 @@ -651,13 +653,14 @@
    1.20        | proc_rews ({name, proc, lhs, ...} :: ps) =
    1.21            if Pattern.matches tsigt (term_of lhs, term_of t) then
    1.22              (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
    1.23 -             case try (fn () => proc signt prems eta_t) () of
    1.24 -               None => (debug true "EXCEPTION in simproc"; proc_rews ps)
    1.25 -             | Some None => (debug false "FAILED"; proc_rews ps)
    1.26 -             | Some (Some raw_thm) =>
    1.27 +             case transform_failure (curry SIMPROC_FAIL name)
    1.28 +                 (fn () => proc signt prems eta_t) () of
    1.29 +               None => (debug false "FAILED"; proc_rews ps)
    1.30 +             | Some raw_thm =>
    1.31                   (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
    1.32                    (case rews (mk_procrule raw_thm) of
    1.33 -                    None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps)
    1.34 +                    None => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^
    1.35 +                      " -- does not match") t; proc_rews ps)
    1.36                    | some => some)))
    1.37            else proc_rews ps;
    1.38    in case eta_t of