equal
deleted
inserted
replaced
198 rls put_asm (thm_of_thm rul) ct of |
198 rls put_asm (thm_of_thm rul) ct of |
199 NONE => rew_once ruls asm ct apno thms |
199 NONE => rew_once ruls asm ct apno thms |
200 | SOME (ct',asm') => |
200 | SOME (ct',asm') => |
201 rew_once ruls (asm union asm') ct' Appl (rul::thms)) |
201 rew_once ruls (asm union asm') ct' Appl (rul::thms)) |
202 | Calc (cc as (op_,_)) => |
202 | Calc (cc as (op_,_)) => |
203 (case get_calculation_ thy cc ct of |
203 (case adhoc_thm thy cc ct of |
204 NONE => rew_once ruls asm ct apno thms |
204 NONE => rew_once ruls asm ct apno thms |
205 | SOME (thmid, thm') => |
205 | SOME (thmid, thm') => |
206 let |
206 let |
207 val pairopt = |
207 val pairopt = |
208 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) |
208 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) |
234 rls put_asm (thm_of_thm rul) ct of |
234 rls put_asm (thm_of_thm rul) ct of |
235 NONE => rew_once ruls asm ct apno thms |
235 NONE => rew_once ruls asm ct apno thms |
236 | SOME (ct',asm') => |
236 | SOME (ct',asm') => |
237 rew_once ruls (asm union asm') ct' Appl (rul::thms)) |
237 rew_once ruls (asm union asm') ct' Appl (rul::thms)) |
238 | Calc (cc as (op_,_)) => |
238 | Calc (cc as (op_,_)) => |
239 (case get_calculation_ thy cc ct of |
239 (case adhoc_thm thy cc ct of |
240 NONE => rew_once ruls asm ct apno thms |
240 NONE => rew_once ruls asm ct apno thms |
241 | SOME (thmid, thm') => |
241 | SOME (thmid, thm') => |
242 let |
242 let |
243 val pairopt = |
243 val pairopt = |
244 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) |
244 rewrite_ thy ((snd o #rew_ord o rep_rls) ruless) |