src/Pure/Isar/locale.ML
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)) =