equal
deleted
inserted
replaced
82 NONE => rew_once lim rts t apno rs' |
82 NONE => rew_once lim rts t apno rs' |
83 | SOME (t', a') => |
83 | SOME (t', a') => |
84 (msg_3 ctxt t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')) |
84 (msg_3 ctxt t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')) |
85 | Rule.Eval (c as (op_, _)) => |
85 | Rule.Eval (c as (op_, _)) => |
86 (msg_4 ctxt op_; |
86 (msg_4 ctxt op_; |
87 case Eval.adhoc_thm (Proof_Context.theory_of ctxt) c t of |
87 case Eval.adhoc_thm ctxt c t of |
88 NONE => rew_once lim rts t apno rs' |
88 NONE => rew_once lim rts t apno rs' |
89 | SOME (thmid, tm) => |
89 | SOME (thmid, tm) => |
90 (let |
90 (let |
91 val (t', a') = case Rewrite.rewrite_ ctxt ro erls true tm t of |
91 val (t', a') = case Rewrite.rewrite_ ctxt ro erls true tm t of |
92 SOME ta => ta |
92 SOME ta => ta |