equal
deleted
inserted
replaced
499 |
499 |
500 val th = |
500 val th = |
501 (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal) |
501 (Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal) |
502 handle THM _ => err_lost ()) |
502 handle THM _ => err_lost ()) |
503 |> Drule.flexflex_unique (SOME ctxt) |
503 |> Drule.flexflex_unique (SOME ctxt) |
504 |> Thm.check_shyps ctxt (Variable.sorts_of ctxt) |
504 |> Thm.check_shyps ctxt |
505 |> Thm.check_hyps (Context.Proof ctxt); |
505 |> Thm.check_hyps (Context.Proof ctxt); |
506 |
506 |
507 val goal_propss = filter_out null propss; |
507 val goal_propss = filter_out null propss; |
508 val results = |
508 val results = |
509 Conjunction.elim_balanced (length goal_propss) th |
509 Conjunction.elim_balanced (length goal_propss) th |
945 val goal_propss = filter_out null propss'; |
945 val goal_propss = filter_out null propss'; |
946 |
946 |
947 val goal = |
947 val goal = |
948 Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss) |
948 Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss) |
949 |> Thm.cterm_of goal_ctxt |
949 |> Thm.cterm_of goal_ctxt |
950 |> Thm.weaken_sorts (Variable.sorts_of goal_ctxt); |
950 |> Thm.weaken_sorts' goal_ctxt; |
951 val statement = ((kind, pos), propss', Thm.term_of goal); |
951 val statement = ((kind, pos), propss', Thm.term_of goal); |
952 |
952 |
953 val after_qed' = after_qed |>> (fn after_local => fn results => |
953 val after_qed' = after_qed |>> (fn after_local => fn results => |
954 map_context (fold Variable.maybe_bind_term result_binds) #> after_local results); |
954 map_context (fold Variable.maybe_bind_term result_binds) #> after_local results); |
955 in |
955 in |