diff -r ff887850d83c -r 92dc6cfa3a95 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Aug 25 20:19:10 2010 +0800
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Aug 25 22:55:42 2010 +0800
@@ -6,22 +6,22 @@
 
 atom_decl name
 
-declare [[STEPS = 20]]
+declare [[STEPS = 21]]
 
 nominal_datatype ty =
   Var "name"
 | Fun "ty" "ty"
 and tys =
-  All xs::"name fset" ty::"ty" bind_res xs in ty
+  All xs::"name fset" ty::"ty" bind (res) xs in ty
+
 
 nominal_datatype ty2 =
   Var2 "name"
 | Fun2 "ty2" "ty2"
 
-instance ty2 :: pt sorry
 
 nominal_datatype tys2 =
-  All2 xs::"name fset" ty::"ty2" bind_res xs in ty
+  All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
 
 
 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]