# HG changeset patch
# User wenzelm
# Date 1572528569 -3600
# Node ID 3ee90f831805517aecf371667abc91504b965d23
# Parent  196b41b9b9c88ef8f08d305c42887429e360891b
clarified signature;

diff -r 196b41b9b9c8 -r 3ee90f831805 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Wed Oct 30 18:30:28 2019 -0400
+++ b/src/Pure/Thy/export_theory.ML	Thu Oct 31 14:29:29 2019 +0100
@@ -255,11 +255,9 @@
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
     fun proof_boxes_of thm thm_id =
-      let
-        val dep_boxes =
-          thm |> Thm_Deps.proof_boxes (fn thm_id' =>
-            if #serial thm_id = #serial thm_id' then false else is_some (lookup_thm_id thm_id'));
-      in dep_boxes @ [thm_id] end;
+      (Thm_Deps.proof_boxes
+        {included = fn thm_id' => #serial thm_id = #serial thm_id',
+         excluded = is_some o lookup_thm_id} [thm]) @ [thm_id];
 
     fun expand_name thm_id (header: Proofterm.thm_header) =
       if #serial header = #serial thm_id then ""
diff -r 196b41b9b9c8 -r 3ee90f831805 src/Pure/thm_deps.ML
--- a/src/Pure/thm_deps.ML	Wed Oct 30 18:30:28 2019 -0400
+++ b/src/Pure/thm_deps.ML	Thu Oct 31 14:29:29 2019 +0100
@@ -12,7 +12,8 @@
   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 proof_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;
 
@@ -82,16 +83,17 @@
 
 (* proof boxes: undefined PThm nodes *)
 
-fun proof_boxes defined thm =
+fun proof_boxes {included, excluded} thms =
   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
+        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 boxes (Thm.thm_deps thm) Inttab.empty) [] end;
+  in Inttab.fold_rev (cons o #2) (fold (fold boxes o Thm.thm_deps) thms Inttab.empty) [] end;
 
 
 (* unused_thms_cmd *)