determine proof boxes from exported proof (NB: thm_boxes is not sufficient due to OfClass proofs);

--- a/src/Pure/Thy/export_theory.ML	Sun Nov 03 18:53:48 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Sun Nov 03 18:55:35 2019 +0100
@@ -249,16 +249,6 @@
 
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
-    fun proof_boxes thm thm_id =
-      let
-        val selection =
-         {included = Proofterm.this_id (SOME thm_id),
-          excluded = is_some o lookup_thm_id};
-        val boxes =
-          map (Proofterm.thm_header_id o #1) (Proofterm.proof_boxes selection [Thm.proof_of thm])
-            handle Proofterm.MIN_PROOF () => Thm_Deps.thm_boxes selection [thm]
-     in boxes @ [thm_id] end;
-
     fun expand_name thm_id (header: Proofterm.thm_header) =
       if #serial header = #serial thm_id then ""
       else
@@ -277,7 +267,6 @@
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
         val thm = clean_thm (Thm.unconstrainT raw_thm);
-        val boxes = proof_boxes thm thm_id;
 
         val proof0 =
           if Proofterm.export_standard_enabled () then
@@ -290,12 +279,11 @@
           if Proofterm.export_proof_boxes_required thy
           then Proofterm.export_proof_boxes [proof] else ();
       in
-        (prop, (deps, (boxes, proof))) |>
+        (prop, deps, proof) |>
           let
             open XML.Encode Term_XML.Encode;
-            fun encode_box {serial, theory_name} = pair int string (serial, theory_name);
             val encode_proof = Proofterm.encode_standard_proof consts;
-          in pair encode_prop (pair (list string) (pair (list encode_box) encode_proof)) end
+          in triple encode_prop (list string) encode_proof end
       end;
 
     fun export_thm (thm_id, thm_name) =

--- a/src/Pure/Thy/export_theory.scala	Sun Nov 03 18:53:48 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala	Sun Nov 03 18:55:35 2019 +0100
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import scala.collection.immutable.SortedMap
+
+
 object Export_Theory
 {
   /** session content **/
@@ -352,16 +355,12 @@
   sealed case class Thm_Id(serial: Long, theory_name: String)
   {
     def pure: Boolean = theory_name == Thy_Header.PURE
-
-    def cache(cache: Term.Cache): Thm_Id =
-      Thm_Id(serial, cache.string(theory_name))
   }
 
   sealed case class Thm(
     entity: Entity,
     prop: Prop,
     deps: List[String],
-    proof_boxes: List[Thm_Id],
     proof: Term.Proof)
   {
     def cache(cache: Term.Cache): Thm =
@@ -369,7 +368,6 @@
         entity.cache(cache),
         prop.cache(cache),
         deps.map(cache.string _),
-        proof_boxes.map(_.cache(cache)),
         cache.proof(proof))
   }
 
@@ -377,18 +375,13 @@
     provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
       {
         val (entity, body) = decode_entity(Kind.THM, tree)
-        val (prop, (deps, (prf_boxes, prf))) =
+        val (prop, deps, prf) =
         {
           import XML.Decode._
           import Term_XML.Decode._
-          def thm_id(body: XML.Body): Thm_Id =
-          {
-            val (serial, theory_name) = pair(long, string)(body)
-            Thm_Id(serial, theory_name)
-          }
-          pair(decode_prop _, pair(list(string), pair(list(thm_id), proof)))(body)
+          triple(decode_prop, list(string), proof)(body)
         }
-        Thm(entity, prop, deps, prf_boxes, prf)
+        Thm(entity, prop, deps, prf)
       })
 
   sealed case class Proof(
@@ -428,6 +421,46 @@
     }
   }
 
+  def read_proof_boxes(
+    store: Sessions.Store,
+    provider: Export.Provider,
+    proof: Term.Proof,
+    suppress: Thm_Id => Boolean = _ => false,
+    cache: Option[Term.Cache] = None): List[(Thm_Id, Proof)] =
+  {
+    var seen = Set.empty[Long]
+    var result = SortedMap.empty[Long, (Thm_Id, Proof)]
+
+    def boxes(prf: Term.Proof)
+    {
+      prf match {
+        case Term.Abst(_, _, p) => boxes(p)
+        case Term.AbsP(_, _, p) => boxes(p)
+        case Term.Appt(p, _) => boxes(p)
+        case Term.AppP(p, q) => boxes(p); boxes(q)
+        case thm: Term.PThm if !seen(thm.serial) =>
+          seen += thm.serial
+          val id = Thm_Id(thm.serial, thm.theory_name)
+          if (!suppress(id)) {
+            val read =
+              if (id.pure) Export_Theory.read_pure_proof(store, id, cache = cache)
+              else Export_Theory.read_proof(provider, id, cache = cache)
+            read match {
+              case Some(p) =>
+                result += (thm.serial -> (id -> p))
+                boxes(p.proof)
+              case None =>
+                error("Missing proof " + thm.serial + " (theory " + quote (thm.theory_name) + ")")
+            }
+          }
+        case _ =>
+      }
+    }
+
+    boxes(proof)
+    result.iterator.map(_._2).toList
+  }
+
 
   /* type classes */
 

--- a/src/Pure/thm_deps.ML	Sun Nov 03 18:53:48 2019 +0100
+++ b/src/Pure/thm_deps.ML	Sun Nov 03 18:55:35 2019 +0100
@@ -12,8 +12,6 @@
   val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
   val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list
   val pretty_thm_deps: theory -> thm list -> Pretty.T
-  val thm_boxes: {included: Proofterm.thm_id -> bool, excluded: Proofterm.thm_id -> bool} ->
-    thm list -> Proofterm.thm_id list
   val unused_thms_cmd: theory list * theory list -> (string * thm) list
 end;
 
@@ -81,21 +79,6 @@
   in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;
 
 
-(* thm boxes: intermediate PThm nodes *)
-
-fun thm_boxes {included, excluded} thms =
-  let
-    fun boxes (i, thm_node) res =
-      let val thm_id = Proofterm.thm_id (i, thm_node) in
-        if Inttab.defined res i orelse (excluded thm_id andalso not (included thm_id))
-        then res
-        else
-          Inttab.update (i, thm_id) res
-          |> fold boxes (Proofterm.thm_node_thms thm_node)
-      end;
-  in Inttab.fold_rev (cons o #2) (fold (fold boxes o Thm.thm_deps) thms Inttab.empty) [] end;
-
-
 (* unused_thms_cmd *)
 
 fun unused_thms_cmd (base_thys, thys) =