proper treatment of self thm_id;
clarified signature;

--- a/src/Pure/Thy/export_theory.ML	Fri Oct 18 16:25:54 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Oct 18 22:44:19 2019 +0200
@@ -259,12 +259,13 @@
         val {pos, ...} = Name_Space.the_entry space name;
       in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end;
 
-    fun encode_thm serial raw_thm =
+    fun encode_thm thm_id raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
-        val boxes =
-          raw_thm |> Thm_Deps.proof_boxes (fn thm_id =>
-            if #serial thm_id = serial then false else is_some (lookup_thm_id thm_id));
+        val dep_boxes =
+          raw_thm |> Thm_Deps.proof_boxes (fn thm_id' =>
+            if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id'));
+        val boxes = dep_boxes @ [thm_id];
 
         val thm = clean_thm raw_thm;
         val (prop, SOME proof) =
@@ -279,10 +280,10 @@
           in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end
       end;
 
-    fun buffer_export_thm (serial, thm_name) =
+    fun buffer_export_thm (thm_id, thm_name) =
       let
-        val markup = entity_markup_thm (serial, thm_name);
-        val body = encode_thm serial (Global_Theory.get_thm_name thy (thm_name, Position.none));
+        val markup = entity_markup_thm (#serial thm_id, thm_name);
+        val body = encode_thm thm_id (Global_Theory.get_thm_name thy (thm_name, Position.none));
       in YXML.buffer (XML.Elem (markup, body)) end;
 
     val _ =

--- a/src/Pure/global_theory.ML	Fri Oct 18 16:25:54 2019 +0200
+++ b/src/Pure/global_theory.ML	Fri Oct 18 22:44:19 2019 +0200
@@ -13,7 +13,7 @@
   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 dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.T) list
   val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
   val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) option
   val get_thms: theory -> xstring -> thm list
@@ -112,7 +112,12 @@
     NONE => Lazy.lazy (fn () => make_thm_names thy)
   | SOME lazy_tab => lazy_tab);
 
-val dest_thm_names = Inttab.dest o Lazy.force o get_thm_names;
+fun dest_thm_names thy =
+  let
+    val theory_name = Context.theory_long_name thy;
+    fun thm_id i = Proofterm.make_thm_id (i, theory_name);
+    val thm_names = Lazy.force (get_thm_names thy);
+  in Inttab.fold_rev (fn (i, thm_name) => cons (thm_id i, thm_name)) thm_names [] end;
 
 fun lookup_thm_id thy =
   let