--- a/Nominal/Nominal2_Base.thy	Mon Jul 18 00:21:51 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Mon Jul 18 10:50:21 2011 +0100
@@ -1088,6 +1088,13 @@
 by (induct xs) (simp_all add: permute_pure)
 
 
+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)"
+  by (cases x) (simp_all, simp add: permute_fun_app_eq)
+
+
 subsubsection {* Equivariance for @{typ "'a fset"} *}
 
 lemma in_fset_eqvt [eqvt]: