equal
deleted
inserted
replaced
584 fun procedure_inst ctxt rtrm qtrm = |
584 fun procedure_inst ctxt rtrm qtrm = |
585 let |
585 let |
586 val thy = ProofContext.theory_of ctxt |
586 val thy = ProofContext.theory_of ctxt |
587 val rtrm' = HOLogic.dest_Trueprop rtrm |
587 val rtrm' = HOLogic.dest_Trueprop rtrm |
588 val qtrm' = HOLogic.dest_Trueprop qtrm |
588 val qtrm' = HOLogic.dest_Trueprop qtrm |
589 val reg_goal = |
589 val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm') |
590 Syntax.check_term ctxt (regularize_trm ctxt (rtrm', qtrm')) |
|
591 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
590 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
592 val inj_goal = |
591 val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm') |
593 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
|
594 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
592 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
595 in |
593 in |
596 Drule.instantiate' [] |
594 Drule.instantiate' [] |
597 [SOME (cterm_of thy rtrm'), |
595 [SOME (cterm_of thy rtrm'), |
598 SOME (cterm_of thy reg_goal), |
596 SOME (cterm_of thy reg_goal), |