src/Pure/meta_simplifier.ML

--- a/src/Pure/meta_simplifier.ML	Fri Oct 12 16:57:07 2001 +0200
+++ b/src/Pure/meta_simplifier.ML	Fri Oct 12 18:29:51 2001 +0200
@@ -934,7 +934,7 @@
         handle TERM _ => reflexive ct
   in gconv 1 end;
 
-(* Rewrite A in !!x1,...x1. A *)
+(* Rewrite A in !!x1,...,xn. A *)
 fun forall_conv cv ct =
   let val p as (ct1, ct2) = Thm.dest_comb ct
   in (case pairself term_of p of