--- a/Nominal/Ex/TypeSchemes.thy	Sat Jan 29 14:26:47 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Sun Jan 30 09:57:37 2011 +0900
@@ -48,7 +48,7 @@
   Var "name"
 | Fun "ty" "ty"
 and tys =
-  All xs::"name fset" ty::"ty" bind (set+) xs in ty
+  All xs::"name fset" ty::"ty" bind (set) xs in ty
 
 thm ty_tys.distinct
 thm ty_tys.induct
@@ -258,8 +258,9 @@
 --"This is exactly the assumption for the properly defined function"
 defer
 apply (simp add: ty_tys.eq_iff)
+apply (subgoal_tac "(atom ` fset xsa - atom ` fset xs) \<sharp>* ([atom ` fset xs]set. T)")
 apply (subst (asm) Abs_eq_iff2)
-apply (simp add: alpha_res.simps)
+apply (simp add: alphas)
 apply (clarify)
 apply (rule trans)
 apply(rule_tac p="p" in supp_perm_eq[symmetric])
@@ -268,7 +269,7 @@
 apply(drule fresh_star_perm_set_conv)
 apply (rule finite_Diff)
 apply (rule finite_supp)
-apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* ([atom ` fset xs]res. subst \<theta>' T)")
+apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* ([atom ` fset xs]set. subst \<theta>' T)")
 apply (metis Un_absorb2 fresh_star_Un)
 apply (simp add: fresh_star_Un)
 apply (rule conjI)
@@ -276,14 +277,24 @@
 apply rule
 apply(simp (no_asm) only: Abs_fresh_iff)
 apply(clarify)
-apply blast
-defer
+apply simp
+apply (simp add: fresh_star_def)
+apply rule
+apply(simp (no_asm) only: Abs_fresh_iff)
+apply(clarify)
+apply(drule_tac a="atom a" in fresh_eqvt_at)
+apply (simp add: supp_Pair finite_supp)
+apply (simp add: fresh_Pair)
+apply(simp add: Abs_fresh_iff)
+apply(simp add: Abs_fresh_iff)
 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
 prefer 2
 apply (rule perm_supp_eq)
 apply (metis Un_absorb2 fresh_star_Un)
-apply simp
---"Would work for 'set' and 'list' bindings, not sure how to do 'set+'."
+apply (simp add: eqvt_at_def)
+apply (simp add: fresh_star_def)
+apply rule
+apply(simp add: Abs_fresh_iff)
 oops