src/Pure/thm.ML

   val force_strip_shyps : bool ref      (* FIXME tmp (since 1995/08/01) *)
   val strip_shyps       : thm -> thm
   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*)
   val assume            : cterm -> thm
   val compress          : thm -> thm

 fun axioms_of thy =
   map (fn (s, _) => (s, get_axiom thy s))
     (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,
   as it could be slow.*)
 fun compress (Thm {sign_ref, der, maxidx, shyps, hyps, prop}) =