diff -r 3c32f91fa771 -r cb3da5b540f2 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 17 17:51:35 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 18 08:37:45 2010 +0100
@@ -25,7 +25,7 @@
 where
   "bv1 (BUnit) = {}"
 | "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
+| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 
 local_setup {* define_raw_fv "Terms.rtrm1"
   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
@@ -58,7 +58,7 @@
 lemma bv1_eqvt[eqvt]:
   shows "(pi \<bullet> bv1 x) = bv1 (pi \<bullet> x)"
   apply (induct x)
-apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt)
+apply (simp_all add: empty_eqvt insert_eqvt atom_eqvt eqvts)
 done
 
 lemma fv_rtrm1_eqvt[eqvt]: