# HG changeset patch
# User paulson
# Date 1124363165 -7200
# Node ID 4ddeef83bd66e072333d2e2475d1b6f085c6f48c
# Parent  b241ba3eb4db8ba0e7ef54f95f7b431e43af3fc9
optimization to incr_indexes?

diff -r b241ba3eb4db -r 4ddeef83bd66 src/Pure/logic.ML
--- 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;