equal
deleted
inserted
replaced
205 end |
205 end |
206 | Rule.Rls_ rls' => |
206 | Rule.Rls_ rls' => |
207 (case rewrite__set_ ctxt (i + 1) put_asm bdv rls' ct of |
207 (case rewrite__set_ ctxt (i + 1) put_asm bdv rls' ct of |
208 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms |
208 SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms |
209 | NONE => rew_once ruls asm ct apno thms) |
209 | NONE => rew_once ruls asm ct apno thms) |
210 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string_PIDE ctxt r ^ "\""); |
210 | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.to_string ctxt r ^ "\""); |
211 val ruls = (#rules o Rule_Set.rep) rls; |
211 val ruls = (#rules o Rule_Set.rep) rls; |
212 val _ = trace_eq1 ctxt i "rls" rls ct |
212 val _ = trace_eq1 ctxt i "rls" rls ct |
213 val (ct', asm') = rew_once ruls [] ct Noap ruls; |
213 val (ct', asm') = rew_once ruls [] ct Noap ruls; |
214 in if ct = ct' then NONE else SOME (ct', distinct op = asm') end |
214 in if ct = ct' then NONE else SOME (ct', distinct op = asm') end |
215 and app_rev ctxt i rrls t = (* apply an Rrls; if not applicable proceed with subterms*) |
215 and app_rev ctxt i rrls t = (* apply an Rrls; if not applicable proceed with subterms*) |