# 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;