--- a/Nominal/Ex/Foo2.thy	Mon Nov 29 08:01:09 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Fri Dec 03 13:51:07 2010 +0000
@@ -64,7 +64,6 @@
   tests by cu
 *}
 
-
 lemma yy:
   assumes a: "p \<bullet> bs \<inter> bs = {}" 
   and     b: "finite bs"
@@ -100,6 +99,8 @@
 apply(simp add: mem_permute_iff)
 done
 
+
+
 lemma Abs_rename_set:
   fixes x::"'a::fs"
   assumes a: "(p \<bullet> bs) \<sharp>* (bs, x)" 
@@ -217,7 +218,7 @@
   fixes c::"'a::fs"
   assumes "\<exists>name. y = Var name \<Longrightarrow> P" 
   and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
-  and     "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" 
+  and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
   and     "\<exists>a1 trm1 a2 trm2.  ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P"
   and     "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
   shows "P"
@@ -230,7 +231,6 @@
 apply(assumption)
 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, [atom name], trm)")
 apply(erule exE)
-apply(rule assms(3))
 apply(insert Abs_rename_list)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="[atom name]" in meta_spec)
@@ -239,12 +239,14 @@
 apply(drule meta_mp)
 apply(simp)
 apply(erule exE)
-apply(rule exI)+
+apply(rule assms(3))
 apply(perm_simp)
 apply(erule conjE)+
-apply(rule conjI)
 apply(assumption)
-apply(simp add: foo.eq_iff)
+apply(clarify)
+apply(simp (no_asm) add: foo.eq_iff)
+apply(perm_simp)
+apply(assumption)
 apply(rule at_set_avoiding1)
 apply(simp)
 apply(simp add: finite_supp)

--- a/Nominal/Nominal2_Abs.thy	Mon Nov 29 08:01:09 2010 +0000
+++ b/Nominal/Nominal2_Abs.thy	Fri Dec 03 13:51:07 2010 +0000
@@ -255,7 +255,7 @@
 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
   apply(rule_tac [!] equivpI)
-  unfolding reflp_def symp_def transp_def
+  unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def
   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
 quotient_definition

--- a/Nominal/nominal_dt_alpha.ML	Mon Nov 29 08:01:09 2010 +0000
+++ b/Nominal/nominal_dt_alpha.ML	Fri Dec 03 13:51:07 2010 +0000
@@ -593,14 +593,20 @@
 
 (** proves the equivp predicate for all alphas **)
 
+val reflp_def' = 
+  @{lemma "reflp R == !x. R x x" by (simp add: reflp_def refl_on_def)}
+
+val symp_def' =
+  @{lemma "symp R == !x y . R x y --> R y x" by (simp add: symp_def sym_def)}
+
 val transp_def' =
   @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" 
-    by (rule eq_reflection, auto simp add: transp_def)}
+    by (rule eq_reflection, auto simp add: trans_def transp_def)}
 
 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = 
   let
-    val refl' = map (fold_rule @{thms reflp_def[THEN eq_reflection]} o atomize) refl
-    val symm' = map (fold_rule @{thms symp_def[THEN eq_reflection]} o atomize) symm
+    val refl' = map (fold_rule [reflp_def'] o atomize) refl
+    val symm' = map (fold_rule [symp_def'] o atomize) symm
     val trans' = map (fold_rule [transp_def'] o atomize) trans
 
     fun prep_goal t =