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 t'; rew_once (lim - 1) (rts @ [(t, r, (t', a'))]) t' Appl rrs')) |
84 (msg_3 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 op_; |
86 (msg_4 op_; |
87 case Eval.adhoc_thm thy c (TermC.uminus_to_string t) of |
87 case Eval.adhoc_thm thy 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_ thy ro erls true tm t of |
91 val (t', a') = case Rewrite.rewrite_ thy ro erls true tm t of |
92 SOME ta => ta |
92 SOME ta => ta |