Quot/Nominal/Terms.thy
changeset 1117 8948319b190e
parent 1111 ee276c9f12f0
child 1119 44cabac6ad3d
--- 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