diff -r 2d9de77d5687 -r 0dd10a900cae Quot/Examples/LamEx.thy
--- a/Quot/Examples/LamEx.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Wed Dec 09 15:57:47 2009 +0100
@@ -56,29 +56,29 @@
 
 print_quotients
 
-quotient_def 
-  Var :: "name \<Rightarrow> lam"
+quotient_def
+  Var :: "Var :: name \<Rightarrow> lam"
 where
-  "Var \<equiv> rVar"
+  "rVar"
 
-quotient_def 
-  App :: "lam \<Rightarrow> lam \<Rightarrow> lam"
+quotient_def
+  App :: "App :: lam \<Rightarrow> lam \<Rightarrow> lam"
 where
-  "App \<equiv> rApp"
+  "rApp"
 
-quotient_def 
-  Lam :: "name \<Rightarrow> lam \<Rightarrow> lam"
+quotient_def
+  Lam :: "Lam :: name \<Rightarrow> lam \<Rightarrow> lam"
 where
-  "Lam \<equiv> rLam"
+  "rLam"
 
 thm Var_def
 thm App_def
 thm Lam_def
 
-quotient_def 
-  fv :: "lam \<Rightarrow> name set"
+quotient_def
+  fv :: "fv :: lam \<Rightarrow> name set"
 where
-  "fv \<equiv> rfv"
+  "rfv"
 
 thm fv_def
 
@@ -88,10 +88,10 @@
   perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"   (unchecked)
 begin
 
-quotient_def 
-  perm_lam :: "'x prm \<Rightarrow> lam \<Rightarrow> lam"
+quotient_def
+  perm_lam :: "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam"
 where
-  "perm_lam \<equiv> (perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam)"
+  "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam"
 
 end
 
@@ -244,4 +244,4 @@
   apply(simp add: var_supp)
   done
 
-end
\ No newline at end of file
+end