diff -r 8a3352cff8d0 -r 78c0a707fb2d Nominal/Ex/AuxNoFCB.thy
--- a/Nominal/Ex/AuxNoFCB.thy	Fri Mar 30 16:08:00 2012 +0200
+++ b/Nominal/Ex/AuxNoFCB.thy	Mon Apr 02 19:52:17 2012 +0200
@@ -302,8 +302,8 @@
   apply (subgoal_tac "(a \<leftrightarrow> g) \<bullet> (x \<leftrightarrow> f) \<bullet> t = (x \<leftrightarrow> f) \<bullet> (a \<leftrightarrow> g) \<bullet> t")
   apply (subgoal_tac "(b \<leftrightarrow> g) \<bullet> (y \<leftrightarrow> f) \<bullet> s = (y \<leftrightarrow> f) \<bullet> (b \<leftrightarrow> g) \<bullet> s")
   apply simp
-  apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt)
-  apply (smt flip_at_base_simps(3) flip_at_simps(1) flip_eqvt permute_eqvt)
+  apply (subst permute_eqvt) apply (simp add: flip_eqvt)
+  apply (subst permute_eqvt) apply (simp add: flip_eqvt)
   apply (simp add: flip_at_base_simps fresh_at_base flip_def)
   done
 
@@ -323,8 +323,8 @@
   apply simp
   apply (simp add: Abs1_eq_iff)
   apply (auto simp add: Abs1_eq_iff flip_def fresh_at_base)[2]
-  apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt)
-  apply (smt atom_eqvt eq_eqvt flip_at_simps(2) flip_def fresh_eqvt)
+  apply (simp add: fresh_permute_left)
+  apply (simp add: fresh_permute_left)
   apply clarify
   apply (simp add: fresh_Cons fresh_Pair fresh_at_base)
   apply clarify