--- a/Quot/Examples/LamEx.thy	Fri Dec 11 08:28:41 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Fri Dec 11 11:08:58 2009 +0100
@@ -57,18 +57,18 @@
 print_quotients
 
 quotient_def
-  Var :: "Var :: name \<Rightarrow> lam"
-where
+   "Var :: name \<Rightarrow> lam"
+as
   "rVar"
 
 quotient_def
-  App :: "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
-where
+   "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
+as
   "rApp"
 
 quotient_def
-  Lam :: "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
-where
+   "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
+as
   "rLam"
 
 thm Var_def
@@ -76,8 +76,8 @@
 thm Lam_def
 
 quotient_def
-  fv :: "fv :: lam \<Rightarrow> name set"
-where
+   "fv :: lam \<Rightarrow> name set"
+as
   "rfv"
 
 thm fv_def
@@ -89,18 +89,12 @@
 begin
 
 quotient_def
-  perm_lam :: "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
-where
+   "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
+as
   "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
 
 end
 
-(*quotient_def (for lam)
-  abs_fun_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
-where
-  "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"*)
-
-
 thm perm_lam_def
 
 (* lemmas that need to lift *)