equal
deleted
inserted
replaced
601 let |
601 let |
602 val thy = ProofContext.theory_of ctxt |
602 val thy = ProofContext.theory_of ctxt |
603 val rtrm' = HOLogic.dest_Trueprop rtrm |
603 val rtrm' = HOLogic.dest_Trueprop rtrm |
604 val qtrm' = HOLogic.dest_Trueprop qtrm |
604 val qtrm' = HOLogic.dest_Trueprop qtrm |
605 val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') |
605 val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') |
606 handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm |
606 handle (ERROR msg) => lift_match_error ctxt msg rtrm qtrm |
607 val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') |
607 val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') |
608 handle (LIFT_MATCH msg) => lift_match_error ctxt msg rtrm qtrm |
608 handle (ERROR msg) => lift_match_error ctxt msg rtrm qtrm |
609 in |
609 in |
610 Drule.instantiate' [] |
610 Drule.instantiate' [] |
611 [SOME (cterm_of thy rtrm'), |
611 [SOME (cterm_of thy rtrm'), |
612 SOME (cterm_of thy reg_goal), |
612 SOME (cterm_of thy reg_goal), |
613 NONE, |
613 NONE, |