diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 04 16:18:07 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.
 *)