# HG changeset patch # User wenzelm # Date 1704753842 -3600 # Node ID a7241e5db6019f85b8e261365c98d03f6665a75a # Parent eb142693255f6f1e24880ebb26cb9c4da01e8ee2 tuned source structure; diff -r eb142693255f -r a7241e5db601 src/Pure/proofterm.ML --- 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'