diff -r 5335c0ea743a -r 313e6f2cdd89 Nominal/Ex/TypeSchemes1.thy
--- a/Nominal/Ex/TypeSchemes1.thy	Thu May 31 12:01:13 2012 +0100
+++ b/Nominal/Ex/TypeSchemes1.thy	Mon Jun 04 21:39:51 2012 +0100
@@ -146,6 +146,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)
@@ -271,8 +272,6 @@
 apply(drule_tac x="atom name" in bspec)
 apply(auto)[1]
 apply(simp add: fresh_def supp_perm)
-apply(perm_simp)
-apply(auto)
 done
 
 nominal_primrec