equal
deleted
inserted
replaced
708 (* global_qed *) |
708 (* global_qed *) |
709 |
709 |
710 fun finish_global state = |
710 fun finish_global state = |
711 let |
711 let |
712 val (_, (((kind, name, t), (_, raw_thm)), _)) = current_goal state; (*ignores after_qed!*) |
712 val (_, (((kind, name, t), (_, raw_thm)), _)) = current_goal state; (*ignores after_qed!*) |
713 val full_name = if name = "" then "" else Sign.full_name (sign_of state) name; |
|
714 val result = |
713 val result = |
715 prep_result state t raw_thm |
714 prep_result state t raw_thm |
716 |> Drule.standard |> Tactic.norm_hhf |
715 |> Drule.standard |> Tactic.norm_hhf; |
717 |> curry Thm.name_thm full_name; |
|
718 |
716 |
719 val atts = |
717 val atts = |
720 (case kind of Theorem (s, atts) => atts @ [Drule.kind s] |
718 (case kind of Theorem (s, atts) => atts @ [Drule.kind s] |
721 | _ => err_malformed "finish_global" state); |
719 | _ => err_malformed "finish_global" state); |
722 |
720 |