--- a/src/Pure/General/symbol.ML Tue May 30 16:02:27 2000 +0200 +++ b/src/Pure/General/symbol.ML Tue May 30 16:02:56 2000 +0200 @@ -247,7 +247,7 @@ -(** scanning though symbols **) +(** scanning through symbols **) fun scanner msg scan chs = let