--- a/RTree.thy	Tue Jul 12 15:09:09 2016 +0100
+++ b/RTree.thy	Tue Aug 16 11:49:37 2016 +0100
@@ -73,9 +73,9 @@
   nodes (including itself) which can reach @{text "x"} by following
   some path in @{text "r"}: *}
 
-definition "subtree r x = {y . (y, x) \<in> r^*}"
+definition "subtree r x = {node' . (node', x) \<in> r^*}"
 
-definition "ancestors r x = {y. (x, y) \<in> r^+}"
+definition "ancestors r x = {node'. (x, node') \<in> r^+}"
 
 definition "root r x = (ancestors r x = {})"
 
@@ -108,7 +108,7 @@
   shows "(a, b) \<notin> edges_in r x"
   using assms by (unfold edges_in_def subtree_def, auto)
 
-definition "children r x = {y. (y, x) \<in> r}"
+definition "children r x = {node'. (node', x) \<in> r}"
 
 locale fforest = forest +
   assumes fb: "finite (children r x)"