diff -r 3acc7d25627a -r 8948319b190e Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 10 11:27:49 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 10 11:31:43 2010 +0100
@@ -936,7 +936,7 @@
   rbv6
 where
   "rbv6 (rVr6 n) = {}"
-| "rbv6 (rLm6 n t) = {atom n}"
+| "rbv6 (rLm6 n t) = {atom n} \<union> rbv6 t"
 | "rbv6 (rLt6 l r) = rbv6 l \<union> rbv6 r"
 
 primrec