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(