--- a/Nominal/Test.thy	Tue Mar 09 22:10:10 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 10 12:48:38 2010 +0100
@@ -141,8 +141,9 @@
   bv1
 where
   "bv1 (BUnit1) = {}"
+| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
 | "bv1 (BV1 x) = {atom x}"
-| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
+
 
 thm bv1_raw.simps
 
@@ -338,12 +339,13 @@
   "cbinders (Type t T) = {atom t}"
 | "cbinders (Dty t) = {atom t}"
 | "cbinders (DStru x s) = {atom x}"
-| "cbinders (Val v M) = {atom v}"
+| "cbinders (Val v M) = {atom v}"*)
 | "Cbinders (Type1 t) = {atom t}"
 | "Cbinders (Type2 t T) = {atom t}"
 | "Cbinders (SStru x S) = {atom x}"
 | "Cbinders (SVal v T) = {atom v}"  
 
+
 (* core haskell *)
 print_theorems