diff -r 5a8a3e209b95 -r 232595afb82e Nominal/Ex/ExLetMult.thy
--- a/Nominal/Ex/ExLetMult.thy	Tue May 04 16:33:38 2010 +0200
+++ b/Nominal/Ex/ExLetMult.thy	Tue May 04 16:42:28 2010 +0200
@@ -1,17 +1,14 @@
 theory ExLetMult
-imports "../Parser"
+imports "../NewParser"
 begin
 
 atom_decl name
 
-ML {* val _ = recursive := true *}
-ML {* val _ = alpha_type := AlphaLst *}
-ML {* val _ = cheat_equivp := true *}
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
-| Lm x::"name" t::"trm" bind x in t
-| Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t, bind "bn l" in s
+| Lm x::"name" t::"trm" bind_set x in t
+| Lt l::"lts" t::"trm" s::"trm" bind "bn l" in t s
 and lts =
   Lnil
 | Lcons "name" "trm" "lts"