diff -r 9a63d90d1752 -r f7c4b8e6918b Nominal/Ex/TypeSchemes2.thy
--- a/Nominal/Ex/TypeSchemes2.thy	Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Ex/TypeSchemes2.thy	Tue Jan 03 11:43:27 2012 +0000
@@ -265,7 +265,7 @@
   apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")
   apply (erule subsetD)
   apply (simp add: supp_eqvt)
-  apply (metis le_eqvt permute_boolI)
+  apply (metis permute_pure subset_eqvt)
   apply (rule perm_supp_eq)
   apply (simp add: fresh_def fresh_star_def)
   apply blast
@@ -307,7 +307,4 @@
   apply auto
   done
 
-
-
-
 end