--- a/src/Pure/Isar/proof.ML Wed Oct 31 19:41:29 2001 +0100
+++ b/src/Pure/Isar/proof.ML Wed Oct 31 19:49:36 2001 +0100
@@ -710,11 +710,9 @@
fun finish_global state =
let
val (_, (((kind, name, t), (_, raw_thm)), _)) = current_goal state; (*ignores after_qed!*)
- val full_name = if name = "" then "" else Sign.full_name (sign_of state) name;
val result =
prep_result state t raw_thm
- |> Drule.standard |> Tactic.norm_hhf
- |> curry Thm.name_thm full_name;
+ |> Drule.standard |> Tactic.norm_hhf;
val atts =
(case kind of Theorem (s, atts) => atts @ [Drule.kind s]