equal
deleted
inserted
replaced
281 let |
281 let |
282 val cx = cert x; |
282 val cx = cert x; |
283 val {T = xT, thy, ...} = Thm.rep_cterm cx; |
283 val {T = xT, thy, ...} = Thm.rep_cterm cx; |
284 val ct = cert (tune t); |
284 val ct = cert (tune t); |
285 in |
285 in |
286 if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct) |
286 if Type.could_unify (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct) |
287 else error (Pretty.string_of (Pretty.block |
287 else error (Pretty.string_of (Pretty.block |
288 [Pretty.str "Ill-typed instantiation:", Pretty.fbrk, |
288 [Pretty.str "Ill-typed instantiation:", Pretty.fbrk, |
289 Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, |
289 Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, |
290 Display.pretty_ctyp (#T (Thm.crep_cterm ct))])) |
290 Display.pretty_ctyp (#T (Thm.crep_cterm ct))])) |
291 end |
291 end |
613 (nth concls (j - 1) + more_consumes) |
613 (nth concls (j - 1) + more_consumes) |
614 (nth_list arbitrary (j - 1)))) |
614 (nth_list arbitrary (j - 1)))) |
615 THEN' inner_atomize_tac) j)) |
615 THEN' inner_atomize_tac) j)) |
616 THEN' atomize_tac) i st |> Seq.maps (fn st' => |
616 THEN' atomize_tac) i st |> Seq.maps (fn st' => |
617 guess_instance (internalize more_consumes rule) i st' |
617 guess_instance (internalize more_consumes rule) i st' |
618 |> Seq.map (rule_instance thy taking) |
618 |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking)) |
619 |> Seq.maps (fn rule' => |
619 |> Seq.maps (fn rule' => |
620 CASES (rule_cases rule' cases) |
620 CASES (rule_cases rule' cases) |
621 (Tactic.rtac rule' i THEN |
621 (Tactic.rtac rule' i THEN |
622 PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) |
622 PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st')))) |
623 THEN_ALL_NEW_CASES rulify_tac |
623 THEN_ALL_NEW_CASES rulify_tac |
670 SUBGOAL_CASES (fn (goal, i) => fn st => |
670 SUBGOAL_CASES (fn (goal, i) => fn st => |
671 ruleq goal |
671 ruleq goal |
672 |> Seq.maps (RuleCases.consume [] facts) |
672 |> Seq.maps (RuleCases.consume [] facts) |
673 |> Seq.maps (fn ((cases, (_, more_facts)), rule) => |
673 |> Seq.maps (fn ((cases, (_, more_facts)), rule) => |
674 guess_instance rule i st |
674 guess_instance rule i st |
675 |> Seq.map (rule_instance thy taking) |
675 |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking)) |
676 |> Seq.maps (fn rule' => |
676 |> Seq.maps (fn rule' => |
677 CASES (make_cases is_open rule' cases) |
677 CASES (make_cases is_open rule' cases) |
678 (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) |
678 (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st))) |
679 end; |
679 end; |
680 |
680 |