--- a/Nominal/Ex/TypeSchemes.thy	Tue Jun 01 15:46:07 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 02 11:37:51 2010 +0200
@@ -5,6 +5,7 @@
 section {*** Type Schemes ***}
 
 atom_decl name
+declare [[STEPS = 9]]
 
 nominal_datatype ty =
   Var "name"
@@ -12,6 +13,15 @@
 and tys =
   All xs::"name fset" ty::"ty" bind_res xs in ty
 
+nominal_datatype ty2 =
+  Var2 "name"
+| Fun2 "ty2" "ty2"
+
+(* PROBLEM: this only works once the type is defined
+nominal_datatype tys2 =
+  All2 xs::"name fset" ty::"ty2" bind_res xs in ty
+*)
+
 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]