--- 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
 

--- a/RTree.thy	Fri Jun 17 09:46:25 2016 +0100
+++ b/RTree.thy	Mon Jun 27 14:08:21 2016 +0100
@@ -1,6 +1,5 @@
 theory RTree
-imports "~~/src/HOL/Library/Transitive_Closure_Table" Max
-        (* "Lcrules" *)
+imports "~~/src/HOL/Library/Transitive_Closure_Table" 
 begin
 
 section {* A theory of relational trees *}
@@ -21,18 +20,10 @@
   {\em single valued} and {\em acyclic}. 
 *}
 
-text {*
-  The following @{text "sgv"} specifies that relation @{text "r"} is {\em single valued}.
-*}
-locale sgv = 
+
+locale rtree = 
   fixes r
   assumes sgv: "single_valued r"
-
-text {*
-  The following @{text "rtree"} specifies that @{text "r"} is a 
-  {\em Relational Tree}.
-*}
-locale rtree = sgv + 
   assumes acl: "acyclic r"
 
 text {*