# HG changeset patch
# User ballarin
# Date 1188909149 -7200
# Node ID ea0f9b8db436f4d6a03261ff06ade4bd821de326
# Parent  6892fdc7e9f8d8feedb92fd2ba12f2b3e9b8fe1c
Improved comment.

diff -r 6892fdc7e9f8 -r ea0f9b8db436 src/Pure/Isar/locale.ML
--- 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)) =