clarified signature;

--- a/src/Pure/Thy/export_theory.ML	Thu Oct 31 14:29:29 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML	Thu Oct 31 21:21:09 2019 +0100
@@ -255,7 +255,7 @@
     val lookup_thm_id = Global_Theory.lookup_thm_id thy;
 
     fun proof_boxes_of thm thm_id =
-      (Thm_Deps.proof_boxes
+      (Thm_Deps.thm_boxes
         {included = fn thm_id' => #serial thm_id = #serial thm_id',
          excluded = is_some o lookup_thm_id} [thm]) @ [thm_id];
 

--- a/src/Pure/thm_deps.ML	Thu Oct 31 14:29:29 2019 +0100
+++ b/src/Pure/thm_deps.ML	Thu Oct 31 21:21:09 2019 +0100
@@ -12,7 +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: {included: Proofterm.thm_id -> bool, excluded: Proofterm.thm_id -> bool} ->
+  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,9 +81,9 @@
   in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;
 
 
-(* proof boxes: undefined PThm nodes *)
+(* thm boxes: intermediate PThm nodes *)
 
-fun proof_boxes {included, excluded} thms =
+fun thm_boxes {included, excluded} thms =
   let
     fun boxes (i, thm_node) res =
       let val thm_id = Proofterm.thm_id (i, thm_node) in