--- a/LamEx.thy	Thu Oct 29 07:29:12 2009 +0100
+++ b/LamEx.thy	Thu Oct 29 08:06:49 2009 +0100
@@ -17,7 +17,6 @@
 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
 
 quotient lam = rlam / alpha
-apply -
 sorry
 
 print_quotients