# HG changeset patch
# User paulson
# Date 1166793844 -3600
# Node ID d0c67d715deb784e5ea93e0be0f99db09aed1a5f
# Parent  9a7949815a84a42c572dbb23bc970a6263990ea4
fixed typo in comment

diff -r 9a7949815a84 -r d0c67d715deb src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Fri Dec 22 14:03:30 2006 +0100
+++ b/src/Pure/General/symbol.ML	Fri Dec 22 14:24:04 2006 +0100
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Generalized characters with and infinite amount of named symbols.
+Generalized characters with infinitely many named symbols.
 *)
 
 signature SYMBOL =