equal
deleted
inserted
replaced
106 (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of |
106 (case try (Drule.instantiate' ty_inst trm_inst) ball_bex_thm of |
107 NONE => NONE |
107 NONE => NONE |
108 | SOME thm' => |
108 | SOME thm' => |
109 (case try (get_match_inst thy (get_lhs thm')) redex of |
109 (case try (get_match_inst thy (get_lhs thm')) redex of |
110 NONE => NONE |
110 NONE => NONE |
111 | SOME inst2 => try (Drule.instantiate inst2) thm')) |
111 | SOME inst2 => try (Drule.instantiate_normalize inst2) thm')) |
112 end |
112 end |
113 |
113 |
114 fun ball_bex_range_simproc ss redex = |
114 fun ball_bex_range_simproc ss redex = |
115 let |
115 let |
116 val ctxt = Simplifier.the_context ss |
116 val ctxt = Simplifier.the_context ss |
488 val thm3 = Raw_Simplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2 |
488 val thm3 = Raw_Simplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} thm2 |
489 val (insp, inst) = |
489 val (insp, inst) = |
490 if ty_c = ty_d |
490 if ty_c = ty_d |
491 then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm) |
491 then make_inst_id (term_of (Thm.lhs_of thm3)) (term_of ctrm) |
492 else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm) |
492 else make_inst (term_of (Thm.lhs_of thm3)) (term_of ctrm) |
493 val thm4 = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3 |
493 val thm4 = Drule.instantiate_normalize ([], [(cterm_of thy insp, cterm_of thy inst)]) thm3 |
494 in |
494 in |
495 Conv.rewr_conv thm4 ctrm |
495 Conv.rewr_conv thm4 ctrm |
496 end |
496 end |
497 | _ => Conv.all_conv ctrm) |
497 | _ => Conv.all_conv ctrm) |
498 |
498 |