--- 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) =