diff -r f2d545b77b31 -r b151399bd2c3 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Thu Jun 24 21:35:11 2010 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Sun Jun 27 21:41:21 2010 +0100
@@ -5,7 +5,8 @@
 section {*** Type Schemes ***}
 
 atom_decl name
-declare [[STEPS = 9]]
+
+declare [[STEPS = 15]]
 
 nominal_datatype ty =
   Var "name"
@@ -17,10 +18,11 @@
   Var2 "name"
 | Fun2 "ty2" "ty2"
 
-(* PROBLEM: this only works once the type is defined
+instance ty2 :: pt sorry
+
 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]