# HG changeset patch
# User berghofe
# Date 999267691 -7200
# Node ID a4651798a12af6efe23a6796a5443e3aa66da2a3
# Parent  197f2e14a7140029876047ae3608abc8d7154c22
Tuned naming of theorems.

diff -r 197f2e14a714 -r a4651798a12a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Aug 31 16:20:19 2001 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Aug 31 16:21:31 2001 +0200
@@ -102,7 +102,6 @@
   val at_bottom: state -> bool
   val local_qed: (state -> state Seq.seq)
     -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit) -> state -> state Seq.seq
-  val name_refN: string
   val global_qed: (state -> state Seq.seq) -> state
     -> (theory * {kind: string, name: string, thm: thm}) Seq.seq
   val begin_block: state -> state
@@ -706,8 +705,6 @@
 
 (* global_qed *)
 
-val name_refN = "name_ref";
-
 fun finish_global state =
   let
     val (_, (((kind, name, t), (_, raw_thm)), _)) = current_goal state;   (*ignores after_qed!*)
@@ -715,7 +712,7 @@
     val result =
       prep_result state t raw_thm
       |> Drule.standard
-      |> Drule.tag_rule (name_refN, [full_name]);
+      |> curry Thm.name_thm full_name;
 
     val atts =
       (case kind of