--- a/Nominal/Ex/Lambda.thy	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Mon Jun 07 11:43:01 2010 +0200
@@ -3,11 +3,12 @@
 begin
 
 atom_decl name
+declare [[STEPS = 9]]
 
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
-| Lam x::"name" l::"lam"  bind_set x in l
+| Lam x::"name" l::"lam"  bind x in l
 
 thm lam.fv
 thm lam.supp