diff -r ca512f9c0b0a -r 58e13de342a5 Nominal/Ex/ExPS3.thy
--- a/Nominal/Ex/ExPS3.thy	Tue May 04 16:22:21 2010 +0200
+++ b/Nominal/Ex/ExPS3.thy	Tue May 04 16:29:11 2010 +0200
@@ -1,17 +1,20 @@
 theory ExPS3
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example 3 from Peter Sewell's bestiary *)
 
 atom_decl name
 
-ML {* val _ = recursive := false  *}
+ML {* val _ = cheat_alpha_eqvt := true *}
+ML {* val _ = cheat_equivp := true *}
+ML {* val _ = cheat_alpha_bn_rsp := true *}
+
 nominal_datatype exp =
   VarP "name"
 | AppP "exp" "exp"
-| LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
+| LamP x::"name" e::"exp" bind_set x in e
+| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
 and pat3 =
   PVar "name"
 | PUnit
@@ -30,7 +33,7 @@
 thm exp_pat3.induct
 thm exp_pat3.distinct
 thm exp_pat3.fv
-thm exp_pat3.supp
+thm exp_pat3.supp(1-2)
 
 end