now uses find to locate .thy.ML files everywhere

--- a/rm-logfiles	Tue Sep 13 10:42:34 1994 +0200
+++ b/rm-logfiles	Tue Sep 13 11:19:38 1994 +0200
@@ -2,6 +2,4 @@
 #rm-logfiles: remove useless files from subdirectories
 rm log */make*.log */make*.log.gz
 rm */test
-rm */.*.thy.ML
-rm */ex/.*.thy.ML
-rm HOL/Subst/.*.thy.ML
+find . -name '.*.thy.ML' -print -exec rm {} \;

--- a/src/Tools/rm-logfiles	Tue Sep 13 10:42:34 1994 +0200
+++ b/src/Tools/rm-logfiles	Tue Sep 13 11:19:38 1994 +0200
@@ -2,6 +2,4 @@
 #rm-logfiles: remove useless files from subdirectories
 rm log */make*.log */make*.log.gz
 rm */test
-rm */.*.thy.ML
-rm */ex/.*.thy.ML
-rm HOL/Subst/.*.thy.ML
+find . -name '.*.thy.ML' -print -exec rm {} \;