--- a/src/Pure/proofterm.ML Mon Jan 08 23:17:32 2024 +0100
+++ b/src/Pure/proofterm.ML Mon Jan 08 23:44:02 2024 +0100
@@ -81,7 +81,6 @@
val get_proofs_level: unit -> int
val proofs: int Unsynchronized.ref
val any_proofs_enabled: unit -> bool
- val compact_proof: proof -> bool
val proof_combt: proof * term list -> proof
val proof_combt': proof * term option list -> proof
val proof_combP: proof * proof list -> proof
@@ -90,6 +89,7 @@
val any_head_of: proof -> proof
val term_head_of: proof -> proof
val proof_head_of: proof -> proof
+ val compact_proof: proof -> bool
val strip_thm_body: proof_body -> proof_body
val map_proof_same: term Same.operation -> typ Same.operation
-> (typ * class -> proof) -> proof Same.operation
@@ -492,16 +492,6 @@
let val proofs = get_proofs_level ()
in zproof_enabled proofs orelse proof_enabled proofs end;
-val atomic_proof =
- (fn Abst _ => false | AbsP _ => false
- | op % _ => false | op %% _ => false
- | MinProof => false
- | _ => true);
-
-fun compact_proof (p % _) = compact_proof p
- | compact_proof (p %% q) = atomic_proof q andalso compact_proof p
- | compact_proof p = atomic_proof p;
-
fun (p %> t) = p % SOME t;
val proof_combt = Library.foldl (op %>);
@@ -530,6 +520,16 @@
fun proof_head_of (p %% _) = proof_head_of p
| proof_head_of p = p;
+val atomic_proof =
+ (fn Abst _ => false | AbsP _ => false
+ | op % _ => false | op %% _ => false
+ | MinProof => false
+ | _ => true);
+
+fun compact_proof (p % _) = compact_proof p
+ | compact_proof (p %% q) = atomic_proof q andalso compact_proof p
+ | compact_proof p = atomic_proof p;
+
fun strip_thm_body (body as PBody {proof, ...}) =
(case term_head_of (proof_head_of proof) of
PThm (_, Thm_Body {body = body', ...}) => Future.join body'