--- a/RTree.thy	Thu Sep 21 14:33:13 2017 +0100
+++ b/RTree.thy	Fri Sep 22 03:08:30 2017 +0100
@@ -1496,7 +1496,9 @@
     show "finite M" .
   qed
   thus ?case
-    by (unfold subtree_children finite_Un, auto)
+    apply(subst subtree_children finite_Un)
+    apply(auto)
+    done  
 qed
 
 end