equal
deleted
inserted
replaced
208 rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) |
208 rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) |
209 rls put_asm thm' ct; |
209 rls put_asm thm' ct; |
210 val _ = if pairopt <> NONE then () |
210 val _ = if pairopt <> NONE then () |
211 else error("rewrite_set_, rewrite_ \""^ |
211 else error("rewrite_set_, rewrite_ \""^ |
212 (ThmC.string_of_thm thm')^"\" \""^ |
212 (ThmC.string_of_thm thm')^"\" \""^ |
213 (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE") |
213 (Syntax.string_of_term (ThyC.to_ctxt thy) ct)^"\" = NONE") |
214 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); |
214 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); |
215 val ruls = (#rules o Rule_Set.rep) ruless; |
215 val ruls = (#rules o Rule_Set.rep) ruless; |
216 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
216 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
217 in if ct = ct' then NONE else SOME (ct',asm') end; |
217 in if ct = ct' then NONE else SOME (ct',asm') end; |
218 |
218 |
244 rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) |
244 rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless) |
245 rls put_asm thm' ct; |
245 rls put_asm thm' ct; |
246 val _ = if pairopt <> NONE then () |
246 val _ = if pairopt <> NONE then () |
247 else error("rewrite_set_, rewrite_ \""^ |
247 else error("rewrite_set_, rewrite_ \""^ |
248 (ThmC.string_of_thm thm')^"\" \""^ |
248 (ThmC.string_of_thm thm')^"\" \""^ |
249 (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE") |
249 (Syntax.string_of_term (ThyC.to_ctxt thy) ct)^"\" = NONE") |
250 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); |
250 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end); |
251 val ruls = (#rules o Rule_Set.rep) ruless; |
251 val ruls = (#rules o Rule_Set.rep) ruless; |
252 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
252 val (ct',asm') = rew_once ruls [] ct Noap ruls; |
253 in if ct = ct' then NONE else SOME (ct',asm') end; |
253 in if ct = ct' then NONE else SOME (ct',asm') end; |
254 |
254 |