diff -r 2a684ee023e7 -r 4c243e6a71b2 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Dec 16 19:24:55 2008 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Tue Dec 16 20:32:41 2008 +0000
@@ -1262,19 +1262,21 @@
   apply (simp add: pt_rev_pi [OF pt at])
   done
 
-lemma insert_eqvt:
+lemma pt_insert_eqvt:
+  fixes pi::"'x prm"
+  and   x::"'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and at: "at TYPE('x)" 
-  shows "(pi::'x prm)\<bullet>(insert (x::'a) X) = insert (pi\<bullet>x) (pi\<bullet>X)"
+  shows "(pi\<bullet>(insert x X)) = insert (pi\<bullet>x) (pi\<bullet>X)"
   by (auto simp add: perm_set_eq [OF pt at])
 
-lemma set_eqvt:
+lemma pt_set_eqvt:
   fixes pi :: "'x prm"
   and   xs :: "'a list"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and at: "at TYPE('x)" 
   shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
-by (induct xs) (auto simp add: empty_eqvt insert_eqvt [OF pt at])
+by (induct xs) (auto simp add: empty_eqvt pt_insert_eqvt [OF pt at])
 
 lemma supp_singleton:
   assumes pt: "pt TYPE('a) TYPE('x)"
@@ -1568,10 +1570,10 @@
 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
 apply(drule_tac x="pi\<bullet>xa" in bspec)
 apply(simp add: pt_set_bij1[OF ptb, OF at])
-apply(simp add: set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
+apply(simp add: pt_set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
 apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
 apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt [OF ptb at])
+apply(simp add: pt_set_bij1[OF ptb, OF at] pt_set_eqvt [OF ptb at])
 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
 done