# HG changeset patch
# User wenzelm
# Date 1566323791 -7200
# Node ID a896257a3f07c4993dbe9d8295820d67bfc53293
# Parent  3a7117c33742ee849add900bd199a23464fdb60e
export thm_deps;

diff -r 3a7117c33742 -r a896257a3f07 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Tue Aug 20 19:49:49 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Tue Aug 20 19:56:31 2019 +0200
@@ -255,13 +255,20 @@
         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;
 
-    val encode_thm = clean_thm #> (fn thm =>
-      standard_prop Name.context
-        (Thm.extra_shyps thm)
-        (Thm.full_prop_of thm)
-        (try Thm.reconstruct_proof_of thm) |>
-      let open XML.Encode Term_XML.Encode
-      in pair encode_prop (option Proofterm.encode_full) end);
+    fun encode_thm raw_thm =
+      let
+        val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy raw_thm);
+        val thm = clean_thm raw_thm;
+        val (prop, proof) =
+          standard_prop Name.context
+            (Thm.extra_shyps thm)
+            (Thm.full_prop_of thm)
+            (try Thm.reconstruct_proof_of thm);
+      in
+        (prop, (deps, proof)) |>
+          let open XML.Encode Term_XML.Encode
+          in pair encode_prop (pair (list string) (option Proofterm.encode_full)) end
+      end;
 
     fun export_thms thms =
       let val elems =
diff -r 3a7117c33742 -r a896257a3f07 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Aug 20 19:49:49 2019 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Aug 20 19:56:31 2019 +0200
@@ -327,23 +327,23 @@
 
   /* theorems */
 
-  sealed case class Thm(entity: Entity, prop: Prop, proof: Option[Term.Proof])
+  sealed case class Thm(entity: Entity, prop: Prop, deps: List[String], proof: Option[Term.Proof])
   {
     def cache(cache: Term.Cache): Thm =
-      Thm(entity.cache(cache), prop.cache(cache), proof.map(cache.proof _))
+      Thm(entity.cache(cache), prop.cache(cache), deps.map(cache.string _), proof.map(cache.proof _))
   }
 
   def read_thms(provider: Export.Provider): List[Thm] =
     provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.THM, tree)
-        val (prop, prf) =
+        val (prop, (deps, prf)) =
         {
           import XML.Decode._
           import Term_XML.Decode._
-          pair(decode_prop _, option(proof))(body)
+          pair(decode_prop _, pair(list(string), option(proof)))(body)
         }
-        Thm(entity, prop, prf)
+        Thm(entity, prop, deps, prf)
       })
 
   def read_proof(