# HG changeset patch # User wenzelm # Date 959695376 -7200 # Node ID 56c44eee46add1bc023738ca33339fdc5d030be7 # Parent da290d99d8b22d46d7039ff52480ae9c3ef3d63f fixed comment; diff -r da290d99d8b2 -r 56c44eee46ad src/Pure/General/symbol.ML --- 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