equal
deleted
inserted
replaced
212 | scan_ f (pp::pps) = |
212 | scan_ f (pp::pps) = |
213 if f pp then true else scan_ f pps; |
213 if f pp then true else scan_ f pps; |
214 in scan_ chk prepat end; |
214 in scan_ chk prepat end; |
215 (* apply the normal_form of a rev-set *) |
215 (* apply the normal_form of a rev-set *) |
216 fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t = |
216 fun app_rev' thy (Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...}) t = |
217 if chk_prepat thy erls prepat t |
217 if chk_prepat thy erls prepat t then normal_form t else NONE; |
218 then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t) |
|
219 else NONE; |
|
220 val opt = app_rev' thy rrls t |
218 val opt = app_rev' thy rrls t |
221 in |
219 in |
222 case opt of |
220 case opt of |
223 SOME (t', asm) => (t', asm, true) |
221 SOME (t', asm) => (t', asm, true) |
224 | NONE => app_sub thy i rrls t |
222 | NONE => app_sub thy i rrls t |