# HG changeset patch
# User wenzelm
# Date 1571338578 -7200
# Node ID 2a318149b01b789af7c8f5b8385db63e51c042a9
# Parent  15adbeb1fabdc4e0773a33055cce6d59408c5ae4
proof boxes based on proof digest (not proof term): thus it works with prune_proofs;

diff -r 15adbeb1fabd -r 2a318149b01b src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Thu Oct 17 20:56:09 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Thu Oct 17 20:56:18 2019 +0200
@@ -248,10 +248,7 @@
 
     (* theorems *)
 
-    val clean_thm =
-      Thm.transfer thy
-      #> Thm.check_hyps (Context.Theory thy)
-      #> Thm.strip_shyps;
+    val clean_thm = Thm.check_hyps (Context.Theory thy) #> Thm.strip_shyps;
 
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
@@ -265,16 +262,16 @@
     fun encode_thm serial raw_thm =
       let
         val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
-        fun defined (thm_id: Proofterm.thm_id) =
-          if #serial thm_id = serial then false else is_some (lookup_thm_id thm_id);
+        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 thm = clean_thm raw_thm;
         val (prop, SOME proof) =
           SOME (if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else MinProof)
           |> standard_prop Name.context (Thm.extra_shyps thm) (Thm.full_prop_of thm);
-        val proof_boxes = Proofterm.proof_boxes defined proof;
       in
-        (prop, (deps, (proof, proof_boxes))) |>
+        (prop, (deps, (proof, boxes))) |>
           let
             open XML.Encode Term_XML.Encode;
             val encode_proof = Proofterm.encode_standard_proof consts;
diff -r 15adbeb1fabd -r 2a318149b01b src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Oct 17 20:56:09 2019 +0200
+++ b/src/Pure/proofterm.ML	Thu Oct 17 20:56:18 2019 +0200
@@ -179,9 +179,9 @@
     (serial * proof_body future) list -> proof_body -> thm * proof
   val get_approximative_name: sort list -> term list -> term -> proof -> string
   type thm_id = {serial: serial, theory_name: string}
+  val make_thm_id: serial * string -> thm_id
   val thm_id: thm -> thm_id
   val get_id: sort list -> term list -> term -> proof -> thm_id option
-  val proof_boxes: (thm_id -> bool) -> proof -> thm_id list
 end
 
 structure Proofterm : PROOFTERM =
@@ -2286,26 +2286,6 @@
   | SOME {name = "", ...} => NONE
   | SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name)));
 
-
-(* proof boxes: undefined PThm nodes *)
-
-fun proof_boxes defined proof =
-  let
-    fun boxes_of (Abst (_, _, prf)) = boxes_of prf
-      | boxes_of (AbsP (_, _, prf)) = boxes_of prf
-      | boxes_of (prf % _) = boxes_of prf
-      | boxes_of (prf1 %% prf2) = boxes_of prf1 #> boxes_of prf2
-      | boxes_of (PThm ({serial = i, theory_name = thy, ...}, thm_body)) =
-          (fn boxes =>
-            if defined (make_thm_id (i, thy)) orelse Inttab.defined boxes i then boxes
-            else
-              let
-                val prf' = thm_body_proof_raw thm_body;
-                val boxes' = Inttab.update (i, thy) boxes;
-              in boxes_of prf' boxes' end)
-      | boxes_of _ = I;
-  in Inttab.fold_rev (cons o make_thm_id) (boxes_of proof Inttab.empty) [] end;
-
 end;
 
 structure Basic_Proofterm =
diff -r 15adbeb1fabd -r 2a318149b01b src/Pure/thm_deps.ML
--- a/src/Pure/thm_deps.ML	Thu Oct 17 20:56:09 2019 +0200
+++ b/src/Pure/thm_deps.ML	Thu Oct 17 20:56:18 2019 +0200
@@ -12,6 +12,7 @@
   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 proof_boxes: (Proofterm.thm_id -> bool) -> thm -> Proofterm.thm_id list
   val unused_thms_cmd: theory list * theory list -> (string * thm) list
 end;
 
@@ -79,6 +80,20 @@
   in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;
 
 
+(* proof boxes: undefined PThm nodes *)
+
+fun proof_boxes defined thm =
+  let
+    fun boxes (i, thm_node) res =
+      let val thm_id = Proofterm.thm_id (i, thm_node) in
+        if defined thm_id orelse Inttab.defined res i 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 boxes (Thm.thm_deps thm) Inttab.empty) [] end;
+
+
 (* unused_thms_cmd *)
 
 fun unused_thms_cmd (base_thys, thys) =