--- a/Nominal/Ex/TypeSchemes1.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/TypeSchemes1.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -80,8 +80,7 @@
 where
   "\<theta><Var X> = lookup \<theta> X"
 | "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)"
-  unfolding eqvt_def subst_graph_def
-  apply (rule, perm_simp, rule)
+  apply(simp add: eqvt_def subst_graph_aux_def)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="b" in ty.exhaust)
@@ -119,8 +118,7 @@
   substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
 where
   "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
-  unfolding eqvt_def substs_graph_def
-  apply (rule, perm_simp, rule)
+  apply(simp add: eqvt_def substs_graph_aux_def)
   apply auto[2]
   apply (rule_tac y="b" and c="a" in tys.strong_exhaust)
   apply auto[1]
@@ -279,10 +277,7 @@
 where
   "atom ` (fset Xs) \<sharp>* T \<Longrightarrow>  
      T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. T = \<theta><T'> \<and> atom ` Dom \<theta> = atom ` fset Xs \<inter> supp T')"
-unfolding generalises_graph_def
-unfolding eqvt_def
-apply(perm_simp)
-apply(simp)
+apply(simp add: generalises_graph_aux_def eqvt_def)
 apply(rule TrueI)
 apply(case_tac x)
 apply(simp)
@@ -409,8 +404,7 @@
 where
   "ftv (Var X) = {|X|}"
 | "ftv (T1 \<rightarrow> T2) = (ftv T1) |\<union>| (ftv T2)"
-  unfolding eqvt_def ftv_graph_def
-  apply (rule, perm_simp, rule)
+  apply(simp add: eqvt_def ftv_graph_aux_def)
   apply(rule TrueI)
   apply(rule_tac y="x" in ty.exhaust)
   apply(blast)