diff -r 0ecc775e5fce -r 790940e90db2 Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 02 08:42:10 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 08:43:53 2010 +0100
@@ -216,43 +216,43 @@
 (* example form Leroy 96 about modules; OTT *)
 
 nominal_datatype mexp =
-  Acc path
-| Stru body
-| Funct x::name sexp m::mexp    bind x in m
-| FApp mexp path
-| Ascr mexp sexp
+  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
+| Seq c::defn d::"body"     bind "cbinders c" in d
 and defn =  
-  Type name tyty
-| Dty name
-| DStru name mexp
-| Val name trmtrm
+  Type "name" "tyty"
+| Dty "name"
+| DStru "name" "mexp"
+| Val "name" "trmtrm"
 and sexp =
   Sig sbody
-| SFunc name sexp sexp
+| SFunc "name" "sexp" "sexp"
 and sbody = 
   SEmpty
-| SSeq C::spec D::sbody  bind "Cbinders C" in D
+| SSeq C::spec D::sbody    bind "Cbinders C" in D
 and spec =
-  Type1 name 
-| Type2 name tyty
-| SStru name sexp
-| SVal name tyty
+  Type1 "name" 
+| Type2 "name" "tyty"
+| SStru "name" "sexp"
+| SVal "name" "tyty"
 and tyty =
-  Tyref1 name
-| Tyref2 path tyty
-| Fun tyty tyty
+  Tyref1 "name"
+| Tyref2 "path" "tyty"
+| Fun "tyty" "tyty"
 and path =
-  Sref1 name
-| Sref2 path name
+  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
+  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"