--- a/src/Pure/Thy/export_theory.ML Thu Oct 31 21:21:09 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML Thu Oct 31 22:34:16 2019 +0100
@@ -254,10 +254,15 @@
val lookup_thm_id = Global_Theory.lookup_thm_id thy;
- fun proof_boxes_of thm thm_id =
- (Thm_Deps.thm_boxes
- {included = fn thm_id' => #serial thm_id = #serial thm_id',
- excluded = is_some o lookup_thm_id} [thm]) @ [thm_id];
+ fun proof_boxes thm thm_id =
+ let
+ val selection =
+ {included = fn thm_id' => #serial thm_id = #serial 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 ""
@@ -277,7 +282,7 @@
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_of thm thm_id;
+ val boxes = proof_boxes thm thm_id;
val proof0 =
if export_standard_proofs then
--- a/src/Pure/proofterm.ML Thu Oct 31 21:21:09 2019 +0100
+++ b/src/Pure/proofterm.ML Thu Oct 31 22:34:16 2019 +0100
@@ -31,6 +31,7 @@
proof: proof}
type oracle = string * term option
type thm = serial * thm_node
+ exception MIN_PROOF of unit
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
val map_proof_of: (proof -> proof) -> proof_body -> proof_body
@@ -188,6 +189,8 @@
val thm_header_id: thm_header -> thm_id
val thm_id: thm -> thm_id
val get_id: sort list -> term list -> term -> proof -> thm_id option
+ val proof_boxes: {excluded: thm_id -> bool, included: thm_id -> bool} ->
+ proof list -> (thm_header * proof) list (*exception MIN_PROOF*)
end
structure Proofterm : PROOFTERM =
@@ -228,6 +231,8 @@
val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
+exception MIN_PROOF of unit;
+
fun proof_of (PBody {proof, ...}) = proof;
val join_proof = Future.join #> proof_of;
@@ -1630,8 +1635,6 @@
local
-exception MIN_PROOF of unit;
-
fun forall_intr_vfs prop = fold_rev Logic.all (variables_of prop) prop;
fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof' (variables_of prop) prf;
@@ -2320,6 +2323,30 @@
| SOME {name = "", ...} => NONE
| SOME {serial, theory_name, ...} => SOME (make_thm_id (serial, theory_name)));
+
+(* proof boxes: intermediate PThm nodes *)
+
+fun proof_boxes {included, excluded} proofs =
+ 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 (header as {serial = i, ...}, thm_body)) =
+ (fn boxes =>
+ let val thm_id = thm_header_id header in
+ if Inttab.defined boxes i orelse (excluded thm_id andalso not (included thm_id))
+ then boxes
+ else
+ let
+ val prf' = thm_body_proof_open thm_body;
+ val boxes' = Inttab.update (i, (header, prf')) boxes;
+ in boxes_of prf' boxes' end
+ end)
+ | boxes_of MinProof = raise MIN_PROOF ()
+ | boxes_of _ = I;
+ in Inttab.fold_rev (cons o #2) (fold boxes_of proofs Inttab.empty) [] end;
+
end;
structure Basic_Proofterm =