# HG changeset patch
# User wenzelm
# Date 1717436601 -7200
# Node ID 07ddd501120af7f1a78b948fa8d0b866234d7ddd
# Parent  d562aabcc8680f5011f5cc116b6ab1ae83cde8d6
removed unused/inefficient size_of_proof (see also 2241191a3c54);

diff -r d562aabcc868 -r 07ddd501120a src/Pure/proofterm.ML
--- 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)