# HG changeset patch
# User berghofe
# Date 1002904191 -7200
# Node ID 0ec18d3131b53878baf2eb56928bc74468c4e81a
# Parent  da6fc37ed6fa34f0b5119417c0f7f28fc4c881ba
Tuned comment.

diff -r da6fc37ed6fa -r 0ec18d3131b5 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