diff -r ad4382e546fc -r c25714ca1c19 src/Tools/rm-logfiles
--- a/src/Tools/rm-logfiles	Tue Nov 05 11:20:52 1996 +0100
+++ b/src/Tools/rm-logfiles	Tue Nov 05 11:48:09 1996 +0100
@@ -3,4 +3,4 @@
 #Remove useless files from subdirectories
 rm log */make*.log */make*.log.gz
 rm */test
-find . -name '.*.thy.ML' -print -exec rm {} \;
+rm */.*.thy.ML */.*.thy.ML */*/.*.thy.ML