--- a/Nominal/Ex/ExLeroy.thy	Tue May 04 11:22:22 2010 +0200
+++ b/Nominal/Ex/ExLeroy.thy	Tue May 04 12:34:33 2010 +0200
@@ -1,21 +1,20 @@
 theory ExLeroy
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example form Leroy 96 about modules; OTT *)
 
 atom_decl name
 
-ML {* val _ = recursive := false  *}
 nominal_datatype mexp =
   Acc "path"
 | Stru "body"
-| Funct x::"name" "sexp" m::"mexp"    bind x in m
+| Funct x::"name" "sexp" m::"mexp"    bind_set x in m
 | FApp "mexp" "path"
 | Ascr "mexp" "sexp"
 and body =
   Empty
-| Seq c::defn d::"body"     bind "cbinders c" in d
+| Seq c::defn d::"body"     bind_set "cbinders c" in d
 and defn =
   Type "name" "tyty"
 | Dty "name"
@@ -26,7 +25,7 @@
 | SFunc "name" "sexp" "sexp"
 and sbody =
   SEmpty
-| SSeq C::spec D::sbody    bind "Cbinders C" in D
+| SSeq C::spec D::sbody    bind_set "Cbinders C" in D
 and spec =
   Type1 "name"
 | Type2 "name" "tyty"
@@ -42,7 +41,7 @@
 and trmtrm =
   Tref1 "name"
 | Tref2 "path" "name"
-| Lam' v::"name" "tyty" M::"trmtrm"  bind v in M
+| Lam' v::"name" "tyty" M::"trmtrm"  bind_set v in M
 | App' "trmtrm" "trmtrm"
 | Let' "body" "trmtrm"
 binder
@@ -65,8 +64,8 @@
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)]
 
 end