--- a/Nominal/Ex/Lambda.thy	Tue May 04 11:12:09 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 04 11:22:22 2010 +0200
@@ -1,5 +1,5 @@
 theory Lambda
-imports "../Parser"
+imports "../NewParser"
 begin
 
 atom_decl name
@@ -7,7 +7,7 @@
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l
+| Lam x::"name" l::"lam"  bind_set x in l
 
 thm lam.fv
 thm lam.supp
@@ -17,7 +17,7 @@
 
 section {* Strong Induction Principles*}
 
-(* 
+(*
   Old way of establishing strong induction
   principles by chosing a fresh name.
 *)