--- a/Nominal/Ex/Lambda_add.thy	Thu Mar 31 15:25:35 2011 +0200
+++ b/Nominal/Ex/Lambda_add.thy	Wed Apr 06 13:47:08 2011 +0100
@@ -3,6 +3,15 @@
 begin
 
 nominal_primrec
+  addlam :: "lam \<Rightarrow> lam"
+where
+  "fv \<noteq> x \<Longrightarrow> addlam (Var x) = Lam [fv]. App (Var fv) (Var x)"
+| "addlam (App t1 t2) = App t1 t2"
+| "addlam (Lam [x]. t) = Lam [x].t"
+oops
+
+
+nominal_primrec
   addlam_pre :: "lam \<Rightarrow> lam \<Rightarrow> lam"
 where
   "fv \<noteq> x \<Longrightarrow> addlam_pre (Var x) (Lam [fv].it) = Lam [fv]. App (Var fv) (Var x)"