src/Pure/Isar/proof.ML
changeset 11992 a39798b57344
parent 11985 06658189cd51
child 12000 715fe3909682
equal deleted inserted replaced
11991:da6ee05d9f3d 11992:a39798b57344
   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;
   713     val full_name = if name = "" then "" else Sign.full_name (sign_of state) name;
   714     val result =
   714     val result =
   715       prep_result state t raw_thm
   715       prep_result state t raw_thm
   716       |> Drule.standard
   716       |> Drule.standard |> Tactic.norm_hhf
   717       |> curry Thm.name_thm full_name;
   717       |> curry Thm.name_thm full_name;
   718 
   718 
   719     val atts =
   719     val atts =
   720       (case kind of Theorem (s, atts) => atts @ [Drule.kind s]
   720       (case kind of Theorem (s, atts) => atts @ [Drule.kind s]
   721       | _ => err_malformed "finish_global" state);
   721       | _ => err_malformed "finish_global" state);