# HG changeset patch
# User wenzelm
# Date 974829899 -3600
# Node ID 6306977d867bd22ac3a914902f1798d08d121a90
# Parent  ea5de7c64c23318a1d1fe0b842b2d5aeb3ff5967
tag result with name reference to final binding (basically just a comment);

diff -r ea5de7c64c23 -r 6306977d867b src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Nov 21 19:04:03 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Nov 21 19:04:59 2000 +0100
@@ -103,6 +103,7 @@
   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
@@ -691,10 +692,16 @@
 
 (* global_qed *)
 
+val name_refN = "name_ref";
+
 fun finish_global state =
   let
     val (_, (((kind, name, t), (_, raw_thm)), _)) = current_goal state;   (*ignores after_qed!*)
-    val result = Drule.standard (prep_result state t raw_thm);
+    val full_name = if name = "" then "" else Sign.full_name (sign_of state) name;
+    val result =
+      prep_result state t raw_thm
+      |> Drule.standard
+      |> Drule.tag_rule (name_refN, [full_name]);
 
     val atts =
       (case kind of