# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272984156 -7200
# Node ID 5aa5c87f7fc039e60fefe6cc03c3c20d3ffe8c8d
# Parent  232595afb82e9e52d7c67c46055e4d87b854efdf# Parent  a58c73e394791d9be7ef65ad9d1c884d90f2dfda
merge

diff -r a58c73e39479 -r 5aa5c87f7fc0 Nominal/Ex/ExLetMult.thy
--- a/Nominal/Ex/ExLetMult.thy	Tue May 04 16:39:12 2010 +0200
+++ b/Nominal/Ex/ExLetMult.thy	Tue May 04 16:42:36 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"