equal
deleted
inserted
replaced
489 in (t, t'', [rs(*one in order to ease locate_rule*)], der) end; |
489 in (t, t'', [rs(*one in order to ease locate_rule*)], der) end; |
490 |
490 |
491 fun locate_rule thy eval_rls ro [rs] t r = |
491 fun locate_rule thy eval_rls ro [rs] t r = |
492 if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r) |
492 if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r) |
493 then |
493 then |
494 let val ropt = Rewrite.rewrite_ (Proof_Context.init_global thy) ro eval_rls true (Rule.thm r) t; |
494 let |
|
495 val ctxt = Proof_Context.init_global thy |
|
496 val ropt = Rewrite.rewrite_ ctxt ro eval_rls true (Rule.thm ctxt r) t; |
495 in |
497 in |
496 case ropt of SOME ta => [(r, ta)] |
498 case ropt of SOME ta => [(r, ta)] |
497 | NONE => ((*tracing |
499 | NONE => ((*tracing |
498 ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) |
500 ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) |
499 end |
501 end |
550 in (t, t'', [rs(*here only _ONE_*)], der) end; |
552 in (t, t'', [rs(*here only _ONE_*)], der) end; |
551 |
553 |
552 fun locate_rule thy eval_rls ro [rs] t r = |
554 fun locate_rule thy eval_rls ro [rs] t r = |
553 if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r) |
555 if member op = ((map (Rule.thm_id)) rs) (Rule.thm_id r) |
554 then |
556 then |
555 let val ropt = Rewrite.rewrite_ (Proof_Context.init_global thy) ro eval_rls true (Rule.thm r) t; |
557 let |
|
558 val ctxt = Proof_Context.init_global thy |
|
559 val ropt = Rewrite.rewrite_ ctxt ro eval_rls true (Rule.thm ctxt r) t; |
556 in |
560 in |
557 case ropt of |
561 case ropt of |
558 SOME ta => [(r, ta)] |
562 SOME ta => [(r, ta)] |
559 | NONE => |
563 | NONE => |
560 ((*tracing ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) |
564 ((*tracing ("### locate_rule: rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) |