--- a/Quot/Nominal/Terms.thy	Wed Feb 17 16:22:16 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 17 17:29:26 2010 +0100
@@ -138,24 +138,20 @@
  "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1"
  "(op = ===> alpha1 ===> alpha1) rLm1 rLm1"
  "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1"
-apply (auto intro: alpha1.intros)
-apply(rule a3) apply (rule_tac x="0" in exI)
+apply (auto simp add: alpha1_inj)
+apply (rule_tac x="0" in exI)
 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
-apply(rule a4) apply assumption apply (rule_tac x="0" in exI)
-apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen)
+apply (rule_tac x="0" in exI)
+apply (simp add: alpha_gen fresh_star_def fresh_zero_perm alpha_rfv1)
 done
 
 lemma [quot_respect]:
   "(op = ===> alpha1 ===> alpha1) permute permute"
-apply auto
-apply (rule alpha1_eqvt)
-apply simp
-done
+  by (simp add: alpha1_eqvt)
 
 lemma [quot_respect]:
   "(alpha1 ===> op =) fv_rtrm1 fv_rtrm1"
-apply (simp add: alpha_rfv1)
-done
+  by (simp add: alpha_rfv1)
 
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
@@ -592,9 +588,10 @@
   "(op = ===> alpha5 ===> alpha5) permute permute"
   "(op = ===> alphalts ===> alphalts) permute permute"
   apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp)
-  apply (auto)
+  apply (clarify) apply (rule conjI)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
+  apply (clarify) apply (rule conjI)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)
   done