diff -r c8acaded1777 -r 4a00077c008f Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Jul 19 19:09:06 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Fri Jul 22 11:37:16 2011 +0100
@@ -529,8 +529,8 @@
 primrec 
   permute_sum 
 where
-  "p \<bullet> (Inl x) = Inl (p \<bullet> x)"
-| "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
+  Inl_eqvt: "p \<bullet> (Inl x) = Inl (p \<bullet> x)"
+| Inr_eqvt: "p \<bullet> (Inr y) = Inr (p \<bullet> y)"
 
 instance 
 by (default) (case_tac [!] x, simp_all)
@@ -545,8 +545,8 @@
 primrec 
   permute_list 
 where
-  "p \<bullet> [] = []"
-| "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
+  Nil_eqvt:  "p \<bullet> [] = []"
+| Cons_eqvt: "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs"
 
 instance 
 by (default) (induct_tac [!] x, simp_all)
@@ -567,8 +567,8 @@
 primrec 
   permute_option 
 where
-  "p \<bullet> None = None"
-| "p \<bullet> (Some x) = Some (p \<bullet> x)"
+  None_eqvt: "p \<bullet> None = None"
+| Some_eqvt: "p \<bullet> (Some x) = Some (p \<bullet> x)"
 
 instance 
 by (default) (induct_tac [!] x, simp_all)