--- a/Nominal/Ex/ExPS7.thy	Tue May 04 12:34:33 2010 +0200
+++ b/Nominal/Ex/ExPS7.thy	Tue May 04 13:52:40 2010 +0200
@@ -1,17 +1,16 @@
 theory ExPS7
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example 7 from Peter Sewell's bestiary *)
 
 atom_decl name
 
-ML {* val _ = recursive := true  *}
 nominal_datatype exp7 =
   EVar name
 | EUnit
 | EPair exp7 exp7
-| ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e
+| ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e
 and lrb =
   Assign name exp7
 and lrbs =