--- a/Nominal/Ex/TypeSchemes.thy	Tue May 25 17:09:29 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Tue May 25 17:29:05 2010 +0200
@@ -178,21 +178,15 @@
 lemma subst_tyS:
   shows "atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T"
   apply (rule strong_induct[of
-    "\<lambda>a t. True" "\<lambda>d T. (atom (fst d) \<sharp> T \<longrightarrow> substs [d] T = T)" _ "t" "(x, S)", simplified])
-  apply (rule impI)
+    "\<lambda>a t. True" "\<lambda>(x, S) T. (atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T)" _ "t" "(x, S)", simplified])
+  apply clarify
   apply (subst s3)
   apply (simp add: fresh_star_def fresh_Cons fresh_Nil)
-  apply (case_tac b)
-  apply clarify
   apply (subst subst_ty)
-  apply simp_all
-  apply (simp add: fresh_star_prod)
-  apply clarify
-  apply (thin_tac "fset_to_set (fmap atom fset) \<sharp>* ba")
+  apply (simp_all add: fresh_star_prod_elim)
   apply (drule fresh_star_atom)
-  apply (unfold fresh_def)
-  apply (simp only: ty_tys.fv[simplified ty_tys.supp])
-  apply (subgoal_tac "atom aa \<notin> fset_to_set (fmap atom fset)")
+  apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])
+  apply (subgoal_tac "atom a \<notin> fset_to_set (fmap atom fset)")
   apply blast
   apply (metis supp_finite_atom_set finite_fset)
   done