src/Pure/Isar/proof.ML
changeset 12000 715fe3909682
parent 11992 a39798b57344
child 12010 e1d4df962ac9
equal deleted inserted replaced
11999:43b4385445bf 12000:715fe3909682
   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