--- a/LamEx.thy	Tue Nov 03 17:30:27 2009 +0100
+++ b/LamEx.thy	Tue Nov 03 17:30:43 2009 +0100
@@ -37,17 +37,17 @@
 
 print_quotients
 
-quotient_def (for lam)
+quotient_def 
   Var :: "name \<Rightarrow> lam"
 where
   "Var \<equiv> rVar"
 
-quotient_def (for lam)
+quotient_def 
   App :: "lam \<Rightarrow> lam \<Rightarrow> lam"
 where
   "App \<equiv> rApp"
 
-quotient_def (for lam)
+quotient_def 
   Lam :: "name \<Rightarrow> lam \<Rightarrow> lam"
 where
   "Lam \<equiv> rLam"
@@ -56,7 +56,7 @@
 thm App_def
 thm Lam_def
 
-quotient_def (for lam)
+quotient_def 
   fv :: "lam \<Rightarrow> name set"
 where
   "fv \<equiv> rfv"
@@ -66,10 +66,10 @@
 (* definition of overloaded permutation function *)
 (* for the lifted type lam                       *)
 overloading
-  perm_lam    \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
+  perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
 begin
 
-quotient_def (for lam)
+quotient_def 
   perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
 where
   "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"
@@ -308,14 +308,11 @@
 thm alpha.induct
 
 lemma rvar_inject: "rVar a \<approx> rVar b \<Longrightarrow> (a = b)"
-apply (rule alpha.cases)
-apply (assumption)
-apply (assumption)
-apply (simp_all)
-apply (cases "a = b")
-apply (simp_all)
-apply (cases "ba = b")
-apply (simp_all)
+apply (erule alpha.cases)
+apply (simp add: rlam.inject)
+apply (simp)
+apply (simp)
+done
 
 
 lemma var_inject_test: