--- 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)