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