optimization to incr_indexes?

--- a/src/Pure/logic.ML	Thu Aug 18 12:11:06 2005 +0200
+++ b/src/Pure/logic.ML	Thu Aug 18 13:06:05 2005 +0200
@@ -202,7 +202,8 @@
 
 (*For all variables in the term, increment indexnames and lift over the Us
     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
-fun incr_indexes (Us, k) t =
+fun incr_indexes ([], 0) t = t
+  | incr_indexes (Us, k) t =
   let
     val n = length Us;
     val incrT = if k = 0 then I else incrT k;