diff -r 5335c0ea743a -r 313e6f2cdd89 Nominal/Nominal2_FCB.thy
--- a/Nominal/Nominal2_FCB.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Nominal2_FCB.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -182,14 +182,14 @@
   then have "q \<bullet> (as \<sharp>* f as x c)"
     by (simp add: permute_bool_def)
   then have "(q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm1)
     using inc fresh1 fr1
     apply(auto simp add: fresh_star_def fresh_Pair)
     done
   then have "(r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
   then have "r \<bullet> (bs \<sharp>* f bs y c)"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm2[symmetric])
     using qq3 fresh2 fr1
     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
@@ -264,7 +264,7 @@
   then have "q \<bullet> ((as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c)"
     by (simp add: permute_bool_def)
   then have "(q \<bullet> (as \<inter> supp x)) \<sharp>* f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm1)
     using inc fresh1 fr1
     apply(auto simp add: fresh_star_def fresh_Pair)
@@ -274,7 +274,7 @@
     apply simp
     done
   then have "r \<bullet> ((bs \<inter> supp y) \<sharp>* f (bs \<inter> supp y) y c)"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm2[symmetric])
     using qq3 fresh2 fr1
     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
@@ -350,14 +350,14 @@
   then have "q \<bullet> ((set as) \<sharp>* f as x c)"
     by (simp add: permute_bool_def)
   then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm1)
     using inc fresh1 fr1
     apply(auto simp add: fresh_star_def fresh_Pair)
     done
   then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
   then have "r \<bullet> ((set bs) \<sharp>* f bs y c)"
-    apply(simp add: fresh_star_eqvt set_eqvt)
+    apply(simp only: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm2[symmetric])
     using qq3 fresh2 fr1
     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)