size_of_proof no longer includes size_of_term

--- a/src/Pure/proofterm.ML	Fri Dec 13 13:47:13 2002 +0100
+++ b/src/Pure/proofterm.ML	Fri Dec 13 14:20:47 2002 +0100
@@ -273,11 +273,9 @@
   (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 (AbsP (_, t, prf)) = 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 (prf % _) = 1 + size_of_proof prf
   | size_of_proof _ = 1;
 
 fun change_type opTs (PThm (name, prf, prop, _)) = PThm (name, prf, prop, opTs)