# HG changeset patch # User berghofe # Date 1039513232 -3600 # Node ID 2241191a3c54305f1e66b719d0048565d1e19e1f # Parent f8f9393be64c5b7f9a9e090d698eab329a88c3d7 Added size_of_proof. diff -r f8f9393be64c -r 2241191a3c54 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Dec 09 10:38:56 2002 +0100 +++ b/src/Pure/proofterm.ML Tue Dec 10 10:40:32 2002 +0100 @@ -47,6 +47,7 @@ val add_prf_tfree_names : string list * proof -> string list val add_prf_tvar_ixns : indexname list * proof -> indexname list val maxidx_of_proof : proof -> int + val size_of_proof : proof -> int val change_type : typ list option -> proof -> proof val prf_abstract_over : term -> proof -> proof val prf_incr_bv : int -> int -> int -> int -> proof -> proof @@ -271,6 +272,14 @@ fun maxidx_of_proof prf = fold_proof_terms (Int.max o apfst maxidx_of_term) (Int.max o apfst maxidx_of_typ) (~1, prf); +fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf + | size_of_proof (AbsP (_, t, prf)) = + if_none (apsome size_of_term t) 1 + size_of_proof prf + | size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2 + | size_of_proof (prf % t) = + if_none (apsome size_of_term t) 1 + size_of_proof prf + | size_of_proof _ = 1; + fun change_type opTs (PThm (name, prf, prop, _)) = PThm (name, prf, prop, opTs) | change_type opTs (PAxm (name, prop, _)) = PAxm (name, prop, opTs) | change_type opTs (Oracle (name, prop, _)) = Oracle (name, prop, opTs)