diff -r 040519ec99e9 -r b52e8651591f Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Nominal2_Base.thy	Thu Mar 13 09:21:31 2014 +0000
@@ -618,7 +618,7 @@
 
 lemma permute_fset_rsp[quot_respect]:
   shows "(op = ===> list_eq ===> list_eq) permute permute"
-  unfolding fun_rel_def
+  unfolding rel_fun_def
   by (simp add: set_eqvt[symmetric])
 
 instantiation fset :: (pt) pt
@@ -1191,8 +1191,8 @@
 
 subsubsection {* Equivariance for @{typ "'a option"} *}
 
-lemma option_map_eqvt[eqvt]:
-  shows "p \<bullet> (Option.map f x) = Option.map (p \<bullet> f) (p \<bullet> x)"
+lemma map_option_eqvt[eqvt]:
+  shows "p \<bullet> (map_option f x) = map_option (p \<bullet> f) (p \<bullet> x)"
   by (cases x) (simp_all)
 
 
@@ -1565,21 +1565,21 @@
   proof -
     { assume "a \<notin> supp p" "a \<notin> supp q"
       then have "(p + q) \<bullet> a = (q + p) \<bullet> a" 
-	by (simp add: supp_perm)
+        by (simp add: supp_perm)
     }
     moreover
     { assume a: "a \<in> supp p" "a \<notin> supp q"
       then have "p \<bullet> a \<in> supp p" by (simp add: supp_perm)
       then have "p \<bullet> a \<notin> supp q" using asm by auto
       with a have "(p + q) \<bullet> a = (q + p) \<bullet> a" 
-	by (simp add: supp_perm)
+        by (simp add: supp_perm)
     }
     moreover
     { assume a: "a \<notin> supp p" "a \<in> supp q"
       then have "q \<bullet> a \<in> supp q" by (simp add: supp_perm)
       then have "q \<bullet> a \<notin> supp p" using asm by auto 
       with a have "(p + q) \<bullet> a = (q + p) \<bullet> a" 
-	by (simp add: supp_perm)
+        by (simp add: supp_perm)
     }
     ultimately show "(p + q) \<bullet> a = (q + p) \<bullet> a" 
       using asm by blast
@@ -2793,19 +2793,19 @@
       by (auto simp: swap_atom)
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> insert a bs \<union> p \<bullet> insert a bs"
-	using ** 
-	apply (auto simp: supp_perm insert_eqvt)
-	apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs")
-	apply(auto)[1]
-	apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
-	apply(blast)
-	apply(simp)
-	done
+        using ** 
+        apply (auto simp: supp_perm insert_eqvt)
+        apply (subgoal_tac "q \<bullet> a \<in> bs \<union> p \<bullet> bs")
+        apply(auto)[1]
+        apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
+        apply(blast)
+        apply(simp)
+        done
       then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
         unfolding supp_swap by auto
       moreover
       have "supp q \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
-	using ** by (auto simp: insert_eqvt)
+        using ** by (auto simp: insert_eqvt)
       ultimately 
       have "supp q' \<subseteq> insert a bs \<union> p \<bullet> insert a bs" 
         unfolding q'_def using supp_plus_perm by blast
@@ -2862,19 +2862,19 @@
       unfolding q'_def using 2 * `a \<notin> set bs` by (auto simp: swap_atom)
     moreover 
     { have "{q \<bullet> a, p \<bullet> a} \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))"
-	using **
-	apply (auto simp: supp_perm insert_eqvt)
-	apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs")
-	apply(auto)[1]
-	apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
-	apply(blast)
-	apply(simp)
-	done
+        using **
+        apply (auto simp: supp_perm insert_eqvt)
+        apply (subgoal_tac "q \<bullet> a \<in> set bs \<union> p \<bullet> set bs")
+        apply(auto)[1]
+        apply(subgoal_tac "q \<bullet> a \<in> {a. q \<bullet> a \<noteq> a}")
+        apply(blast)
+        apply(simp)
+        done
       then have "supp (q \<bullet> a \<rightleftharpoons> p \<bullet> a) \<subseteq> set (a # bs) \<union> p \<bullet> set (a # bs)" 
         unfolding supp_swap by auto
       moreover
       have "supp q \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
-	using ** by (auto simp: insert_eqvt)
+        using ** by (auto simp: insert_eqvt)
       ultimately 
       have "supp q' \<subseteq> set (a # bs) \<union> p \<bullet> (set (a # bs))" 
         unfolding q'_def using supp_plus_perm by blast