--- a/Nominal/Test.thy	Thu Feb 25 12:24:37 2010 +0100
+++ b/Nominal/Test.thy	Thu Feb 25 14:20:10 2010 +0100
@@ -27,7 +27,7 @@
 nominal_datatype trm' =
   Var "name"
 | App "trm'" "trm'"
-| Lam x::"name" t::"trm'"        bind x in t 
+| Lam x::"name" t::"trm'"          bind x in t 
 | Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t
 and pat' =
   PN
@@ -195,6 +195,58 @@
   "bv9 (Var9 x) = {}"
 | "bv9 (Lam9 x b) = {atom x}"
 
+(* example form Leroy 96 about modules *)
+
+nominal_datatype mexp =
+  Acc path
+| Stru body
+| Funct x::name sexp m::mexp    bind x in m
+| FApp mexp path
+| Ascr mexp sexp
+and body =
+  Empty
+| Seq c::defn d::body bind "cbinders c" in d
+and defn =  
+  Type name tyty
+| Dty name
+| DStru name mexp
+| Val name trmtrm
+and sexp =
+  Sig sbody
+| SFunc name sexp sexp
+and sbody = 
+  SEmpty
+| SSeq C::spec D::sbody  bind "Cbinders C" in D
+and spec =
+  Type1 name 
+| Type2 name tyty
+| SStru name sexp
+| SVal name tyty
+and tyty =
+  Tyref1 name
+| Tyref2 path tyty
+| Fun tyty tyty
+and path =
+  Sref1 name
+| Sref2 path name
+and trmtrm =
+  Tref1 name
+| Tref2 path name
+| Lam v::name tyty M::trmtrm  bind v in M
+| App trmtrm trmtrm
+| Let body trmtrm
+binder
+    cbinders :: "defn \<Rightarrow> atom set"
+and Cbinders :: "spec \<Rightarrow> atom set"
+where
+  "cbinders (Type t T) = {atom t}"
+| "cbinders (Dty t) = {atom t}"
+| "cbinders (DStru x s) = {atom x}"
+| "cbinders (Val v M) = {atom v}"
+| "Cbinders (Type1 t) = {atom t}"
+| "Cbinders (Type2 t T) = {atom t}"
+| "Cbinders (SStru x S) = {atom x}"
+| "Cbinders (SVal v T) = {atom v}"  
 
 (* core haskell *)