--- a/Nominal/Ex/TypeSchemes2.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/TypeSchemes2.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -173,7 +173,7 @@
 apply (simp add: eqvts)
 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
 apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp add: fresh_star_permute_iff)
+apply (simp only: fresh_star_permute_iff)
 apply(perm_simp)
 apply(assumption)
 apply(simp (no_asm_use) only: eqvts)
@@ -186,7 +186,7 @@
 apply (simp add: eqvts)
 apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
 apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp add: fresh_star_permute_iff)
+apply (simp only: fresh_star_permute_iff)
 apply(perm_simp)
 apply(assumption)
 apply(simp)
@@ -252,6 +252,7 @@
   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
   apply (simp add: alphas fresh_star_zero)
   apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
+  apply(simp)
   apply blast
   apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
   apply (simp add: supp_Pair eqvts eqvts_raw)
@@ -263,8 +264,11 @@
   apply (simp add: fresh_star_def fresh_def)
   apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric])
   apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")
-  apply (erule subsetD)
-  apply (simp add: supp_eqvt)
+  apply (erule_tac subsetD)
+  apply(simp only: supp_eqvt)
+  apply(perm_simp)
+  apply(drule_tac x="p" in spec)
+  apply(simp)
   apply (metis permute_pure subset_eqvt)
   apply (rule perm_supp_eq)
   apply (simp add: fresh_def fresh_star_def)