diff -r 7687f97eca53 -r d8750d1aaed9 Nominal/Ex/TypeSchemes.thy --- 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 \ T \ substs [(x, S)] T = T" apply (rule strong_induct[of - "\a t. True" "\d T. (atom (fst d) \ T \ substs [d] T = T)" _ "t" "(x, S)", simplified]) - apply (rule impI) + "\a t. True" "\(x, S) T. (atom x \ T \ 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) \* 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 \ fset_to_set (fmap atom fset)") + apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp]) + apply (subgoal_tac "atom a \ fset_to_set (fmap atom fset)") apply blast apply (metis supp_finite_atom_set finite_fset) done