diff -r 040519ec99e9 -r b52e8651591f Nominal/Ex/Pi.thy
--- a/Nominal/Ex/Pi.thy	Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Ex/Pi.thy	Thu Mar 13 09:21:31 2014 +0000
@@ -130,20 +130,20 @@
 
 lemma testl:
   assumes a: "\<exists>y. f = Inl y"
-  shows "(p \<bullet> (Sum_Type.Projl f)) = Sum_Type.Projl (p \<bullet> f)"
+  shows "(p \<bullet> (Sum_Type.projl f)) = Sum_Type.projl (p \<bullet> f)"
 using a by auto
 
 lemma testrr:
   assumes a: "\<exists>y. f = Inr (Inr y)"
-  shows "(p \<bullet> (Sum_Type.Projr (Sum_Type.Projr f))) = Sum_Type.Projr (Sum_Type.Projr (p \<bullet> f))"
+  shows "(p \<bullet> (Sum_Type.projr (Sum_Type.projr f))) = Sum_Type.projr (Sum_Type.projr (p \<bullet> f))"
 using a by auto
 
 lemma testlr:
   assumes a: "\<exists>y. f = Inr (Inl y)"
-  shows "(p \<bullet> (Sum_Type.Projl (Sum_Type.Projr f))) = Sum_Type.Projl (Sum_Type.Projr (p \<bullet> f))"
+  shows "(p \<bullet> (Sum_Type.projl (Sum_Type.projr f))) = Sum_Type.projl (Sum_Type.projr (p \<bullet> f))"
 using a by auto
 
-nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (sum_case (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
+nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (case_sum (\<lambda>x. Inr (Inl undefined)) (\<lambda>x. Inr (Inr undefined)))")
   subsGuard_mix :: "guardedTerm_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> guardedTerm_mix"  ("_[_::=\<onesuperior>\<onesuperior>_]" [100, 100, 100] 100) and
   subsList_mix  :: "sumList_mix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> sumList_mix"          ("_[_::=\<onesuperior>\<twosuperior>_]" [100, 100, 100] 100) and
   subs_mix      :: "piMix \<Rightarrow> name \<Rightarrow> name \<Rightarrow> piMix"                      ("_[_::=\<onesuperior>_]" [100, 100, 100] 100)
@@ -240,33 +240,33 @@
 apply (metis Inr_not_Inl)
 apply (metis Inr_inject Inr_not_Inl)
 apply (metis Inr_inject Inr_not_Inl)
-apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr
-                            (Sum_Type.Projr
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
+                            (Sum_Type.projr
                               (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
 apply clarify
 apply (rule the1_equality)
 apply blast apply assumption
-apply (rule_tac x="Sum_Type.Projr
-                       (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
-                      Sum_Type.Projr
-                       (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply (rule_tac x="Sum_Type.projr
+                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+                      Sum_Type.projr
+                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
 apply clarify
 apply (rule the1_equality)
 apply blast apply assumption
-apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr
-                                                    (Sum_Type.Projr
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
+                                                    (Sum_Type.projr
 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
 apply clarify
 apply (rule the1_equality)
 apply blast apply assumption
-apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl
-                          (Sum_Type.Projr
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
+                          (Sum_Type.projr
                             (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
 apply clarify
 apply (rule the1_equality)
 apply blast apply assumption
-apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr
-                                           (Sum_Type.Projr
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
+                                           (Sum_Type.projr
                                              (subsGuard_mix_subsList_mix_subs_mix_sum
                                                (Inr (Inr (Pb, xb, y)))))" in exI)
 apply clarify
@@ -333,33 +333,33 @@
 apply (metis Inr_not_Inl)
 apply (metis Inr_inject Inr_not_Inl)
 apply (metis Inr_inject Inr_not_Inl)
-apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr
-                            (Sum_Type.Projr
+apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.projr
+                            (Sum_Type.projr
                               (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
 apply clarify
 apply (rule the1_equality)
 apply blast apply assumption
-apply (rule_tac x="Sum_Type.Projr
-                       (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
-                      Sum_Type.Projr
-                       (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
+apply (rule_tac x="Sum_Type.projr
+                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior>
+                      Sum_Type.projr
+                       (Sum_Type.projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI)
 apply clarify
 apply (rule the1_equality)
 apply blast apply assumption
-apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr
-                                                    (Sum_Type.Projr
+apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.projr
+                                                    (Sum_Type.projr
 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI)
 apply clarify
 apply (rule the1_equality)
 apply blast apply assumption
-apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl
-                          (Sum_Type.Projr
+apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.projl
+                          (Sum_Type.projr
                             (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI)
 apply clarify
 apply (rule the1_equality)
 apply blast apply assumption
-apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr
-                                           (Sum_Type.Projr
+apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.projr
+                                           (Sum_Type.projr
                                              (subsGuard_mix_subsList_mix_subs_mix_sum
                                                (Inr (Inr (Pb, xb, y)))))" in exI)
 apply clarify