--- a/Nominal/Ex/TypeVarsTest.thy	Thu Jul 09 02:32:46 2015 +0100
+++ b/Nominal/Ex/TypeVarsTest.thy	Thu Jul 09 09:12:44 2015 +0100
@@ -18,20 +18,21 @@
           bn
         where "bn ANil = []" | "bn (ACons x t as) = (atom x) # (bn as)"
 
+(* NEEDS FIXING
 nominal_datatype ('ann::fs) exp2 =
-  Var var
-| App "'ann exp2" var
-| LetA as::"'ann assn2" body::"'ann exp2" binds "bnn as" in body as
-| Lam x::var body::"'ann exp2" binds x in body
+  Var2 var
+| App2 "'ann exp2" var
+| LetA2 as::"'ann assn2" body::"'ann exp2" binds "bn2 as" in body as
+| Lam2 x::var body::"'ann exp2" binds x in body
 and ('ann::fs) assn2 =
-  ANil 
-| ACons var "'ann exp2" 'ann "'ann assn2"
+  ANil2 
+| ACons2 var "'ann exp2" 'ann "'ann assn2"
 binder
-  bnn :: "('ann::fs) assn2 \<Rightarrow> atom list"
+  bn2 :: "('ann::fs) assn2 \<Rightarrow> atom list"
 where 
-  "bnn ANil = []" 
-| "bnn (ACons x a t as) = (atom x) # (bnn as)"
-
+  "bn2 ANil2 = []" 
+| "bn2 (ACons2 x a t as) = (atom x) # (bn2 as)"
+*)
 
 (* a nominal datatype with type variables and sorts *)
 
@@ -49,11 +50,11 @@
 instance int :: s2 .. 
 
 nominal_datatype ('a::s1, 'b::s2, 'c::at) lam =
-  Var "name"
-| App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
-| Lam x::"name" l::"('a, 'b, 'c) lam"  binds x in l
-| Foo "'a" "'b"
-| Bar x::"'c" l::"('a, 'b, 'c) lam"  binds x in l   (* Bar binds a polymorphic atom *)
+  Var3 "name"
+| App3 "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
+| Lam3 x::"name" l::"('a, 'b, 'c) lam"  binds x in l
+| Foo3 "'a" "'b"
+| Bar3 x::"'c" l::"('a, 'b, 'c) lam"  binds x in l   (* Bar binds a polymorphic atom *)
 
 term Foo
 term Bar