diff -r 040519ec99e9 -r b52e8651591f Nominal/Ex/TypeSchemes2.thy
--- a/Nominal/Ex/TypeSchemes2.thy	Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Ex/TypeSchemes2.thy	Thu Mar 13 09:21:31 2014 +0000
@@ -41,27 +41,27 @@
 
 lemma TEST1:
   assumes "x = Inl y"
-  shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)"
+  shows "(p \<bullet> Sum_Type.projl x) = Sum_Type.projl (p \<bullet> x)"
 using assms by simp
 
 lemma TEST2:
   assumes "x = Inr y"
-  shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)"
+  shows "(p \<bullet> Sum_Type.projr x) = Sum_Type.projr (p \<bullet> x)"
 using assms by simp
 
 lemma test:
   assumes a: "\<exists>y. f x = Inl y"
-  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
-using a
-by (metis Inl_eqvt Projl_Inl permute_fun_app_eq)
+  shows "(p \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl ((p \<bullet> f) (p \<bullet> x))"
+using a TEST1
+by (metis eqvt_bound eqvt_lambda permute_eq_iff)
 
 lemma test2:
   assumes a: "\<exists>y. f x = Inl y"
-  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
+  shows "(p \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl (p \<bullet> (f x))"
 using a
 by clarsimp
 
-nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
+nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
 where
@@ -103,8 +103,8 @@
 apply clarify
 apply (rule the1_equality)
 apply blast apply assumption
-apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
-                  (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
+apply (rule_tac x="(Fun (Sum_Type.projl (subst_substs_sum (Inl (\<theta>, T1))))
+                  (Sum_Type.projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
 apply clarify
 apply (rule the1_equality)
 apply blast apply assumption