src/Pure/global_theory.ML

   val alias_fact: binding -> string -> theory -> theory
   val hide_fact: bool -> string -> theory -> theory
   val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
   val dest_thm_names: theory -> (serial * Thm_Name.T) list
   val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
-  val lookup_thm: theory -> thm -> Thm_Name.T option
+  val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) option
   val get_thms: theory -> xstring -> thm list
   val get_thm: theory -> xstring -> thm
   val transfer_theories: theory -> thm -> thm
   val all_thms_of: theory -> bool -> (string * thm) list
   val get_thm_name: theory -> Thm_Name.T * Position.T -> thm

         NONE => NONE
       | SOME lazy_tab => Inttab.lookup (Lazy.force lazy_tab) (#serial thm_id));
   in lookup end;
 
 fun lookup_thm thy =
-  let val lookup = lookup_thm_id thy
-  in fn thm => (case Thm.derivation_id thm of NONE => NONE | SOME thm_id => lookup thm_id) end;
+  let val lookup = lookup_thm_id thy in
+    fn thm =>
+      (case Thm.derivation_id thm of
+        NONE => NONE
+      | SOME thm_id =>
+          (case lookup thm_id of
+            NONE => NONE
+          | SOME thm_name => SOME (thm_id, thm_name)))
+  end;
 
 val _ =
   Theory.setup (Theory.at_end (fn thy =>
     if is_some (thm_names_of thy) then NONE
     else