--- a/Quot/Nominal/LamEx.thy	Fri Feb 12 15:50:43 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Fri Feb 12 16:04:10 2010 +0100
@@ -282,22 +282,22 @@
 
 quotient_definition
   "Var :: name \<Rightarrow> lam"
-as
+is
   "rVar"
 
 quotient_definition
    "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "rApp"
 
 quotient_definition
   "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "rLam"
 
 quotient_definition
   "fv :: lam \<Rightarrow> atom set"
-as
+is
   "rfv"
 
 lemma perm_rsp[quot_respect]:
@@ -346,7 +346,7 @@
 
 quotient_definition
   "permute_lam :: perm \<Rightarrow> lam \<Rightarrow> lam"
-as
+is
   "permute :: perm \<Rightarrow> rlam \<Rightarrow> rlam"
 
 lemma permute_lam [simp]: