author | ballarin |
Tue, 04 Sep 2007 14:32:29 +0200 | |
changeset 24525 | ea0f9b8db436 |
parent 24524 | 6892fdc7e9f8 |
child 24526 | 7fa202789bf6 |
--- a/src/Pure/Isar/locale.ML Mon Sep 03 16:50:53 2007 +0200 +++ b/src/Pure/Isar/locale.ML Tue Sep 04 14:32:29 2007 +0200 @@ -2007,7 +2007,7 @@ (* abstraction of equations *) -(* maps f(t1,...,tn) to (f(t1,...,tk), [tk+1,...,tn]) where tk is not a variable *) +(* maps f(t1,...,tn) to (f(t1,...,tk), [tk+1,...,tn]) where tk is not a variable and all ti with i>k are *) fun strip_vars ct = let fun stripc (p as (ct, cts)) =