changeset 24525 | ea0f9b8db436 |
parent 24020 | ed4d7abffee7 |
child 24638 | 69cb317edf73 |
--- 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)) =