Tuned comment.
authorberghofe
Fri Oct 12 18:29:51 2001 +0200 (2001-10-12)
changeset 117370ec18d3131b5
parent 11736 da6fc37ed6fa
child 11738 7c7a902a5c65
Tuned comment.
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Fri Oct 12 16:57:07 2001 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Fri Oct 12 18:29:51 2001 +0200
     1.3 @@ -934,7 +934,7 @@
     1.4          handle TERM _ => reflexive ct
     1.5    in gconv 1 end;
     1.6  
     1.7 -(* Rewrite A in !!x1,...x1. A *)
     1.8 +(* Rewrite A in !!x1,...,xn. A *)
     1.9  fun forall_conv cv ct =
    1.10    let val p as (ct1, ct2) = Thm.dest_comb ct
    1.11    in (case pairself term_of p of