--- a/src/Pure/ML-Systems/polyml.ML Sun Sep 07 17:46:44 2008 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Sun Sep 07 17:48:49 2008 +0200 @@ -56,4 +56,3 @@ in use_text tune str_of_pos (1, name) output verbose txt end; end; -