--- a/src/Pure/proofterm.ML Sun Jun 02 14:11:09 2024 +0200
+++ b/src/Pure/proofterm.ML Mon Jun 03 19:43:21 2024 +0200
@@ -100,7 +100,6 @@
val fold_proof_terms: (term -> 'a -> 'a) -> proof -> 'a -> 'a
val fold_proof_terms_types: (term -> 'a -> 'a) -> (typ -> 'a -> 'a) -> proof -> 'a -> 'a
val maxidx_proof: proof -> int -> int
- val size_of_proof: proof -> int
val change_types: typ list option -> proof -> proof
val abstract_over: term -> proof -> proof
val incr_bv_same: int -> int -> int -> int -> proof Same.operation
@@ -595,12 +594,6 @@
fun maxidx_proof prf = fold_proof_terms_types Term.maxidx_term Term.maxidx_typ prf;
-fun size_of_proof (Abst (_, _, prf)) = 1 + size_of_proof prf
- | size_of_proof (AbsP (_, _, prf)) = 1 + size_of_proof prf
- | size_of_proof (prf % _) = 1 + size_of_proof prf
- | size_of_proof (prf1 %% prf2) = size_of_proof prf1 + size_of_proof prf2
- | size_of_proof _ = 1;
-
fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
| change_types (SOME [T]) (PClass (_, c)) = PClass (T, c)
| change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)