--- a/Quot/Nominal/LamEx.thy	Thu Jan 28 12:24:49 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Thu Jan 28 12:25:38 2010 +0100
@@ -230,18 +230,16 @@
 
 lemma alpha_equivp:
   shows "equivp alpha"
-apply(rule equivpI)
-unfolding reflp_def symp_def transp_def
-apply(auto intro: alpha_refl alpha_sym alpha_trans)
-done
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto intro: alpha_refl alpha_sym alpha_trans)
+  done
 
 lemma alpha_rfv:
   shows "t \<approx> s \<Longrightarrow> rfv t = rfv s"
-apply(induct rule: alpha.induct)
-apply(simp)
-apply(simp)
-apply(simp)
-done
+  apply(induct rule: alpha.induct)
+  apply(simp_all)
+  done
 
 
 quotient_type lam = rlam / alpha
@@ -377,6 +375,10 @@
   shows "(Var a = Var b) = (a = b)"
   and   "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)"
 apply(lifting rlam.inject(1) rlam.inject(2))
+apply(regularize)
+prefer 2
+apply(regularize)
+prefer 2
 apply(auto)
 apply(drule alpha.cases)
 apply(simp_all)
@@ -397,18 +399,18 @@
   and   "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')"
   and   "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)"
 apply auto
-apply(erule alpha.cases)
-apply simp_all
-apply(erule alpha.cases)
-apply simp_all
-apply(erule alpha.cases)
-apply simp_all
-apply(erule alpha.cases)
-apply simp_all
-apply(erule alpha.cases)
-apply simp_all
-apply(erule alpha.cases)
-apply simp_all
+apply (erule alpha.cases)
+apply (simp_all only: rlam.distinct)
+apply (erule alpha.cases)
+apply (simp_all only: rlam.distinct)
+apply (erule alpha.cases)
+apply (simp_all only: rlam.distinct)
+apply (erule alpha.cases)
+apply (simp_all only: rlam.distinct)
+apply (erule alpha.cases)
+apply (simp_all only: rlam.distinct)
+apply (erule alpha.cases)
+apply (simp_all only: rlam.distinct)
 done
 
 lemma lam_distinct[simp]: