# HG changeset patch
# User berghofe
# Date 1039785647 -3600
# Node ID 6844c38d74dfd7fba2e87c132106a58a0b4d9537
# Parent  bd410072083317fd9e69c562d1d4dc8aba7e09a9
size_of_proof no longer includes size_of_term

diff -r bd4100720833 -r 6844c38d74df src/Pure/proofterm.ML
--- 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)