--- a/Nominal/Ex/TypeSchemes.thy	Tue May 04 11:08:30 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Tue May 04 11:12:09 2010 +0200
@@ -1,18 +1,16 @@
 theory TypeSchemes
-imports "../Parser"
+imports "../NewParser"
 begin
 
 section {*** Type Schemes ***}
 
 atom_decl name
 
-ML {* val _ = alpha_type := AlphaRes *}
-
 nominal_datatype ty =
   Var "name"
 | Fun "ty" "ty"
 and tys =
-  All xs::"name fset" ty::"ty" bind xs in ty
+  All xs::"name fset" ty::"ty" bind_res xs in ty
 
 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
 
@@ -125,21 +123,21 @@
   apply(simp add: ty_tys.eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alphas)
-  apply(simp add: fresh_star_def fresh_zero_perm)
+  apply(simp add: fresh_star_def fresh_zero_perm supp_at_base)
   done
 
 lemma
   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
   apply(simp add: ty_tys.eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alphas fresh_star_def eqvts)
+  apply(simp add: alphas fresh_star_def eqvts supp_at_base)
   done
 
 lemma
   shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
   apply(simp add: ty_tys.eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff)
+  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
 done
 
 lemma
@@ -148,7 +146,7 @@
   using a
   apply(simp add: ty_tys.eq_iff)
   apply(clarify)
-  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff)
+  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
   apply auto
   done