--- a/src/Pure/ML-Systems/thread_dummy.ML Sun Sep 07 17:48:49 2008 +0200 +++ b/src/Pure/ML-Systems/thread_dummy.ML Sun Sep 07 17:48:50 2008 +0200 @@ -79,4 +79,3 @@ end; end; end; -