--- a/LamEx.thy	Tue Oct 27 14:59:00 2009 +0100
+++ b/LamEx.thy	Tue Oct 27 15:00:15 2009 +0100
@@ -17,8 +17,11 @@
 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
 
 quotient lam = rlam / alpha
+apply -
 sorry
 
+print_quotients
+
 local_setup {*
   make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>
   make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>