diff -r bccda961a612 -r 1a6593bc494d Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Tue May 24 19:39:38 2011 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Wed May 25 21:38:50 2011 +0200
@@ -184,15 +184,14 @@
 apply (case_tac x)
 apply simp apply clarify 
 apply (rule_tac y="b" in ty_tys.exhaust(1))
-apply (auto simp add: ty_tys.eq_iff)[1]
-apply (auto simp add: ty_tys.eq_iff)[1]
-apply blast
+apply (auto)[1]
+apply (auto)[1]
 apply simp apply clarify 
 apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))
-apply (auto simp add: ty_tys.eq_iff)[1]
-apply (auto simp add: ty_tys.distinct)
-apply (auto simp add: ty_tys.eq_iff ty_tys.distinct)[2]
+apply (auto)[1]
+apply (auto)[5]
 --"LAST GOAL"
+apply(simp del: ty_tys.eq_iff)
 thm meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]
 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
@@ -230,7 +229,6 @@
 apply clarify
 --"This is exactly the assumption for the properly defined function"
 defer
-apply (simp add: ty_tys.eq_iff)
 apply (simp only: Abs_eq_res_set)
 apply (subgoal_tac "(atom ` fset xsa \<inter> supp Ta - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
 apply (subst (asm) Abs_eq_iff2)
@@ -361,8 +359,6 @@
 apply(blast)
 apply(blast)
 apply(simp_all add: ty2.distinct)
-apply(simp add: ty2.eq_iff)
-apply(simp add: ty2.eq_iff)
 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)")
 apply(simp add: eqvt_def)
 apply(rule allI)