--- a/Nominal/Nominal2_Base.thy	Tue Jun 14 14:07:07 2011 +0100
+++ b/Nominal/Nominal2_Base.thy	Tue Jun 14 19:11:44 2011 +0100
@@ -1697,12 +1697,10 @@
 subsection {* helper functions for nominal_functions *}
 
 lemma THE_defaultI2:
-  assumes "P a" "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
+  assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
   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 (p \<bullet> d) (p \<bullet> P))"
@@ -1728,22 +1726,16 @@
   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
+  using eqvt[simplified eqvt_def]
   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 THE_defaultI2) 
   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(perm_simp)
+  using eqvt[simplified eqvt_def]
   apply(simp)
-  apply(rule THE_defaultI'[OF ex1])
   done
 
 lemma fundef_ex1_eqvt_at:
@@ -1756,7 +1748,6 @@
   using assms
   by (auto intro: fundef_ex1_eqvt)
 
-(* fixme: polish *)
 lemma fundef_ex1_prop:
   fixes x::"'a::pt"
   assumes f_def: "f == (\<lambda>x::'a. THE_default (d x) (G x))"
@@ -1767,7 +1758,6 @@
   using ex1
   apply(erule_tac ex1E)
   apply(rule THE_defaultI2)
-  apply(assumption)
   apply(blast)
   apply(rule P_all)
   apply(assumption)