--- a/Nominal/Nominal2_Base.thy	Thu Jun 02 22:24:33 2011 +0900
+++ b/Nominal/Nominal2_Base.thy	Thu Jun 02 15:35:33 2011 +0100
@@ -1709,20 +1709,6 @@
   apply(rule THE_defaultI'[OF unique])
   done
 
-lemma fundef_ex1_eqvt2:
-  fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
-  assumes eqvt: "eqvt_at G x"
-  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)
-  using eqvt
-  unfolding eqvt_at_def
-  apply(simp)
-  done
-
 lemma fundef_ex1_eqvt:
   fixes x::"'a::pt"
   assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
@@ -1737,16 +1723,6 @@
   apply(simp add: permute_fun_app_eq)
   done
 
-lemma fundef_ex1_eqvt_at2:
-  fixes x::"'a::pt"
-  assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"
-  assumes eqvt: "eqvt_at G x"
-  assumes ex1: "\<exists>!y. G x y"
-  shows "eqvt_at f x"
-  unfolding eqvt_at_def
-  using assms
-  by (auto intro: fundef_ex1_eqvt2)
-
 lemma fundef_ex1_eqvt_at:
   fixes x::"'a::pt"
   assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))"