--- a/Nominal/Ex/TypeSchemes.thy	Tue Jun 07 08:52:59 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jun 07 10:40:06 2011 +0100
@@ -174,6 +174,7 @@
 apply(assumption)
 apply(simp)
 --"Eqvt done"
+apply(rule TrueI)
 apply (case_tac x)
 apply simp apply clarify 
 apply (rule_tac y="b" in ty_tys.exhaust(1))
@@ -344,6 +345,7 @@
 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"
   unfolding eqvt_def subst_graph_def
   apply (rule, perm_simp, rule)
+  apply(rule TrueI)
   apply(case_tac x)
   apply(simp)
   apply(rule_tac y="b" in ty2.exhaust)
@@ -384,7 +386,7 @@
   "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"
   unfolding eqvt_def substs_graph_def
   apply (rule, perm_simp, rule)
-  apply auto[1]
+  apply auto[2]
   apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
   apply auto
   apply (subst (asm) Abs_eq_res_set)