diff -r e15621aa8c72 -r 337e1b135d2f src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -31,7 +31,7 @@
     sessions_structure: Sessions.Structure,
     session_name: String,
     progress: Progress = new Progress,
-    cache: Term.Cache = Term.make_cache()): Session =
+    cache: Term.Cache = Term.Cache.make()): Session =
   {
     val thys =
       sessions_structure.build_requirements(List(session_name)).flatMap(session =>
@@ -42,7 +42,7 @@
             yield {
               progress.echo("Reading theory " + theory)
               read_theory(Export.Provider.database(db, store.xz_cache, session, theory),
-                session, theory, cache = Some(cache))
+                session, theory, cache = cache)
             }
           }
         }))
@@ -107,7 +107,7 @@
   }
 
   def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
-    cache: Option[Term.Cache] = None): Theory =
+    cache: Term.Cache = Term.Cache.none): Theory =
   {
     val parents =
       if (theory_name == Thy_Header.PURE) Nil
@@ -134,7 +134,7 @@
         read_typedefs(provider),
         read_datatypes(provider),
         read_spec_rules(provider))
-    if (cache.isDefined) theory.cache(cache.get) else theory
+    if (cache.no_cache) theory else theory.cache(cache)
   }
 
   def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A =
@@ -151,11 +151,11 @@
     })
   }
 
-  def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
+  def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.Cache.none): Theory =
     read_pure(store, read_theory(_, _, _, cache = cache))
 
   def read_pure_proof(
-      store: Sessions.Store, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
+      store: Sessions.Store, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] =
     read_pure(store, (provider, _, _) => read_proof(provider, id, cache = cache))
 
 
@@ -375,7 +375,7 @@
   }
 
   def read_proof(
-    provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
+    provider: Export.Provider, id: Thm_Id, cache: Term.Cache = Term.Cache.none): Option[Proof] =
   {
     for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) }
     yield {
@@ -391,7 +391,7 @@
       val proof = Term_XML.Decode.proof_env(env)(proof_body)
 
       val result = Proof(typargs, args, prop, proof)
-      cache.map(result.cache(_)) getOrElse result
+      if (cache.no_cache) result else result.cache(cache)
     }
   }
 
@@ -400,7 +400,7 @@
     provider: Export.Provider,
     proof: Term.Proof,
     suppress: Thm_Id => Boolean = _ => false,
-    cache: Option[Term.Cache] = None): List[(Thm_Id, Proof)] =
+    cache: Term.Cache = Term.Cache.none): List[(Thm_Id, Proof)] =
   {
     var seen = Set.empty[Long]
     var result = SortedMap.empty[Long, (Thm_Id, Proof)]