author | berghofe |
Fri, 12 Oct 2001 18:29:51 +0200 | |
changeset 11737 | 0ec18d3131b5 |
parent 11736 | da6fc37ed6fa |
child 11738 | 7c7a902a5c65 |
--- 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