--- a/Nominal/ExTySch.thy	Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/ExTySch.thy	Mon Mar 29 00:30:47 2010 +0200
@@ -5,13 +5,15 @@
 (* Type Schemes *)
 atom_decl name
 
-(*ML {* val _ = alpha_type := AlphaRes *}*)
+ML {* val _ = alpha_type := AlphaRes *}
 nominal_datatype t =
   Var "name"
 | Fun "t" "t"
 and tyS =
   All xs::"name fset" ty::"t" bind xs in ty
 
+lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
+
 lemma size_eqvt_raw:
   "size (pi \<bullet> t :: t_raw) = size t"
   "size (pi \<bullet> ts :: tyS_raw) = size ts"
@@ -69,8 +71,6 @@
 thm t_tyS.distinct
 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 
-lemmas t_tyS_supp = t_tyS.fv[simplified t_tyS.supp]
-
 lemma induct:
   assumes a1: "\<And>name b. P b (Var name)"
   and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
@@ -120,7 +120,6 @@
   apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alphas)
-  apply(auto)
   apply(simp add: fresh_star_def fresh_zero_perm)
   done
 
@@ -128,16 +127,15 @@
   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
   apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alpha_gen fresh_star_def eqvts)
-  apply auto
+  apply(simp add: alphas fresh_star_def eqvts)
   done
 
 lemma
   shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
   apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
-oops
+  apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
+done
 
 lemma
   assumes a: "a \<noteq> b"
@@ -145,7 +143,7 @@
   using a
   apply(simp add: t_tyS.eq_iff)
   apply(clarify)
-  apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
+  apply(simp add: alphas fresh_star_def eqvts t_tyS.eq_iff)
   apply auto
   done