--- a/PIPBasics.thy	Fri Jun 17 09:46:25 2016 +0100
+++ b/PIPBasics.thy	Mon Jun 27 14:08:21 2016 +0100
@@ -2837,7 +2837,7 @@
 
 lemma rtree_RAG: "rtree (RAG s)"
   using sgv_RAG acyclic_RAG
-  by (unfold rtree_def rtree_axioms_def sgv_def, auto)
+  by (unfold rtree_def, auto)
 
 end