--- a/Nominal-General/Nominal2_Base.thy	Sat Sep 18 05:13:42 2010 +0800
+++ b/Nominal-General/Nominal2_Base.thy	Sat Sep 18 06:09:43 2010 +0800
@@ -140,7 +140,7 @@
 
 lemma Rep_perm_ext:
   "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2"
-  by (simp add: expand_fun_eq Rep_perm_inject [symmetric])
+  by (simp add: fun_eq_iff Rep_perm_inject [symmetric])
 
 
 subsection {* Permutations form a group *}
@@ -224,11 +224,11 @@
 lemma swap_cancel:
   "(a \<rightleftharpoons> b) + (a \<rightleftharpoons> b) = 0"
   by (rule Rep_perm_ext) 
-     (simp add: Rep_perm_simps expand_fun_eq)
+     (simp add: Rep_perm_simps fun_eq_iff)
 
 lemma swap_self [simp]:
   "(a \<rightleftharpoons> a) = 0"
-  by (rule Rep_perm_ext, simp add: Rep_perm_simps expand_fun_eq)
+  by (rule Rep_perm_ext, simp add: Rep_perm_simps fun_eq_iff)
 
 lemma minus_swap [simp]:
   "- (a \<rightleftharpoons> b) = (a \<rightleftharpoons> b)"
@@ -237,7 +237,7 @@
 lemma swap_commute:
   "(a \<rightleftharpoons> b) = (b \<rightleftharpoons> a)"
   by (rule Rep_perm_ext)
-     (simp add: Rep_perm_swap expand_fun_eq)
+     (simp add: Rep_perm_swap fun_eq_iff)
 
 lemma swap_triple:
   assumes "a \<noteq> b" and "c \<noteq> b"
@@ -245,7 +245,7 @@
   shows "(a \<rightleftharpoons> c) + (b \<rightleftharpoons> c) + (a \<rightleftharpoons> c) = (a \<rightleftharpoons> b)"
   using assms
   by (rule_tac Rep_perm_ext)
-     (auto simp add: Rep_perm_simps expand_fun_eq)
+     (auto simp add: Rep_perm_simps fun_eq_iff)
 
 
 section {* Permutation Types *}
@@ -1872,7 +1872,7 @@
     apply (cut_tac `atom a \<sharp> P`)
     apply (simp add: fresh_conv_MOST)
     apply (elim MOST_rev_mp, rule MOST_I, clarify)
-    apply (simp add: permute_fun_def permute_pure expand_fun_eq)
+    apply (simp add: permute_fun_def permute_pure fun_eq_iff)
     apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
     apply (rule refl)
     done
@@ -1896,7 +1896,7 @@
     apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)
     apply (simp add: fresh_conv_MOST)
     apply (elim MOST_rev_mp, rule MOST_I, clarify)
-    apply (simp add: permute_fun_def permute_pure expand_fun_eq)
+    apply (simp add: permute_fun_def permute_pure fun_eq_iff)
     apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
     apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
     apply (rule refl)