author | paulson |
Thu, 18 Aug 2005 13:06:05 +0200 | |
changeset 17120 | 4ddeef83bd66 |
parent 17119 | b241ba3eb4db |
child 17121 | 4c225f640b89 |
src/Pure/logic.ML | file | annotate | diff | comparison | revisions |
--- 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;