# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265797903 -3600
# Node ID 8948319b190eefa7644666cd977387e8151773cf
# Parent  3acc7d25627acd5f3fb877f1885de836aa9d1d19
Fixed rbv6, when translating to OTT.

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