# HG changeset patch
# User berghofe
# Date 1004554176 -3600
# Node ID 715fe3909682aaaa6083306b927f99d5c80c1fc7
# Parent  43b4385445bfa8ad615f2f2d50dda70397606e9e
Removed name_thm from finish_global.

diff -r 43b4385445bf -r 715fe3909682 src/Pure/Isar/proof.ML
--- 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]