--- a/Nominal/Nominal2_Base.thy	Tue Jun 14 11:43:06 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jun 14 14:07:07 2011 +0100
@@ -1701,9 +1701,11 @@
   shows "Q (THE_default d P)"
 by (iprover intro: assms THE_defaultI')
 
+thm THE_default1_equality
+
 lemma the_default_eqvt:
   assumes unique: "\<exists>!x. P x"
-  shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))"
+  shows "(p \<bullet> (THE_default d P)) = (THE_default (p \<bullet> d) (p \<bullet> P))"
   apply(rule THE_default1_equality [symmetric])
   apply(rule_tac p="-p" in permute_boolE)
   apply(simp add: ex1_eqvt)
@@ -1716,21 +1718,37 @@
 
 lemma fundef_ex1_eqvt:
   fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))"
   assumes eqvt: "eqvt G"
   assumes ex1: "\<exists>!y. G x y"
   shows "(p \<bullet> (f x)) = f (p \<bullet> x)"
   apply(simp only: f_def)
   apply(subst the_default_eqvt)
   apply(rule ex1)
+  apply(rule THE_default1_equality [symmetric])
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
   using eqvt
   unfolding eqvt_def
-  apply(simp add: permute_fun_app_eq)
+  apply(simp)
+  apply(rule ex1)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(subst permute_fun_app_eq)
+  back
+  apply(subst the_default_eqvt)
+  apply(rule_tac p="-p" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
+  apply(rule ex1)
+  apply(perm_simp add: permute_minus_cancel)
+  using eqvt
+  unfolding eqvt_def
+  apply(simp)
+  apply(rule THE_defaultI'[OF ex1])
   done
 
 lemma fundef_ex1_eqvt_at:
   fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))"
   assumes eqvt: "eqvt G"
   assumes ex1: "\<exists>!y. G x y"
   shows "eqvt_at f x"
@@ -1741,7 +1759,7 @@
 (* fixme: polish *)
 lemma fundef_ex1_prop:
   fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
+  assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))"
   assumes P_all: "\<And>x y. G x y \<Longrightarrow> P x y"
   assumes ex1: "\<exists>!y. G x y"
   shows "P x (f x)"