diff -r 9866dffd387d -r cbcd4997dac5 Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 02 08:49:04 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 08:58:28 2010 +0100
@@ -25,6 +25,7 @@
 thm alpha_lam_raw_alpha_bp_raw.intros
 thm fv_lam_raw_fv_bp_raw.simps
 
+
 print_theorems
 
 text {* example 2 *}
@@ -39,11 +40,11 @@
 | PS "name"
 | PD "name" "name"
 binder
-  f::"pat' \<Rightarrow> name set"
+  f::"pat' \<Rightarrow> atom set"
 where 
   "f PN = {}"
-| "f (PS x) = {x}"
-| "f (PD x y) = {x, y}"
+| "f (PS x) = {atom x}"
+| "f (PD x y) = {atom x, atom y}"
 
 thm f_raw.simps
 
@@ -57,24 +58,32 @@
 | PS0 "name"
 | PD0 "pat0" "pat0"
 binder
-  f0::"pat0 \<Rightarrow> name set"
+  f0::"pat0 \<Rightarrow> atom set"
 where 
   "f0 PN0 = {}"
-| "f0 (PS0 x) = {x}"
+| "f0 (PS0 x) = {atom x}"
 | "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
 
 thm f0_raw.simps
 
 text {* example type schemes *}
 
-datatype t = 
+(* does not work yet 
+nominal_datatype t = 
   Var "name" 
 | Fun "t" "t"
 
 nominal_datatype tyS = 
-  All xs::"name list" ty::"t" bind xs in ty
+  All xs::"name list" ty::"t_raw" bind xs in ty
+*)
 
-
+(* also does not work
+nominal_datatype t = 
+  Var "name" 
+| Fun "t" "t"
+and  tyS = 
+  All xs::"name list" ty::"t" bind xs in ty
+*)
 
 (* example 1 from Terms.thy *)
 
@@ -128,10 +137,12 @@
 
 (* example 4 from Terms.thy *)
 
+(* does not work yet
 nominal_datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
 | Lm4 x::"name" t::"trm4"  bind x in t
+*)
 
 (* example 5 from Terms.thy *)
 
@@ -277,16 +288,17 @@
   TY tvar
 | CO co
 
-datatype kind = 
+nominal_datatype kind = 
   KStar
 | KFun kind kind
 | KEq kind kind
 
 (* there are types, coercion types and regular types *)
+(*
 nominal_datatype ty =
   TVar tvar
 | TFun string "ty list"
-| TAll tvar kind ty --"some binding"
+| TAll tvar kind_raw ty --"some binding"
 | TSym ty
 | TCir ty ty
 | TApp ty ty
@@ -296,15 +308,16 @@
 | TRightc ty
 | TLeftc ty
 | TCoe ty ty
-
+*)
 typedecl ty --"hack since ty is not yet defined"
 
 abbreviation 
   "atoms A \<equiv> atom ` A"
 
+(* does not work yet
 nominal_datatype trm =
   Var var
-| LAM tv::tvar kind t::trm   bind tv in t 
+| LAM tv::tvar kind_raw t::trm   bind tv in t 
 | APP trm ty
 | Lam v::var ty t::trm       bind v in t
 | App trm trm
@@ -314,12 +327,12 @@
 and assoc = 
   A p::pat t::trm bind "bv p" in t 
 and pat = 
-  K string "(tvar \<times> kind) list" "(var \<times> ty) list"
+  K string "(tvar \<times> kind_raw) list" "(var \<times> ty) list"
 binder
  bv :: "pat \<Rightarrow> atom set"
 where
  "bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
-
+*)
 
 thm bv_raw.simps