# HG changeset patch
# User wenzelm
# Date 878056247 -3600
# Node ID 09b77900af0fe62cd9579e32b3738285a6635fe7
# Parent  63878e2587a730b72c7435b7f8020da9a5f25fab
added name_of_thm;
improved name_thm: does not overwrite existing name;

diff -r 63878e2587a7 -r 09b77900af0f src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Oct 28 17:29:48 1997 +0100
+++ b/src/Pure/thm.ML	Tue Oct 28 17:30:47 1997 +0100
@@ -100,6 +100,7 @@
   val implies_intr_shyps: thm -> thm
   val get_axiom         : theory -> xstring -> thm
   val name_thm          : string * thm -> thm
+  val name_of_thm	: thm -> string
   val axioms_of         : theory -> (string * thm) list
 
   (*meta rules*)
@@ -603,13 +604,18 @@
     (Symtab.dest (#axioms (rep_theory thy)));
 
 (*Attach a label to a theorem to make proof objects more readable*)
-fun name_thm (name, th as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) = 
-    Thm {sign_ref = sign_ref, 
-         der = Join (Theorem name, [der]),
-         maxidx = maxidx,
-         shyps = shyps, 
-         hyps = hyps, 
-         prop = prop};
+fun name_thm (name, th as Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =
+  (case der of
+    Join (Theorem _, _) => th
+  | Join (Axiom _, _) => th
+  | _ => Thm {sign_ref = sign_ref, der = Join (Theorem name, [der]),
+      maxidx = maxidx, shyps = shyps, hyps = hyps, prop = prop});
+
+fun name_of_thm (Thm {der, ...}) =
+  (case der of
+    Join (Theorem name, _) => name
+  | Join (Axiom (_, name), _) => name
+  | _ => "");
 
 
 (*Compression of theorems -- a separate rule, not integrated with the others,