equal
deleted
inserted
replaced
649 |
649 |
650 fun proc_rews ([]:simproc list) = None |
650 fun proc_rews ([]:simproc list) = None |
651 | proc_rews ({name, proc, lhs, ...} :: ps) = |
651 | proc_rews ({name, proc, lhs, ...} :: ps) = |
652 if Pattern.matches tsigt (term_of lhs, term_of t) then |
652 if Pattern.matches tsigt (term_of lhs, term_of t) then |
653 (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t; |
653 (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t; |
654 case proc signt prems eta_t of |
654 case try (fn () => proc signt prems eta_t) () of |
655 None => (debug false "FAILED"; proc_rews ps) |
655 None => (debug true "EXCEPTION in simproc"; proc_rews ps) |
656 | Some raw_thm => |
656 | Some None => (debug false "FAILED"; proc_rews ps) |
|
657 | Some (Some raw_thm) => |
657 (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm; |
658 (trace_thm false ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm; |
658 (case rews (mk_procrule raw_thm) of |
659 (case rews (mk_procrule raw_thm) of |
659 None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps) |
660 None => (trace_cterm false "IGNORED - does not match" t; proc_rews ps) |
660 | some => some))) |
661 | some => some))) |
661 else proc_rews ps; |
662 else proc_rews ps; |