diff -r d1d09177ec89 -r 3ce1089cdbf3 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Fri Dec 31 13:31:39 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Fri Dec 31 15:37:04 2010 +0000
@@ -12,7 +12,7 @@
   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 (set+) xs in ty
 
 thm ty_tys.distinct
 thm ty_tys.induct
@@ -35,7 +35,7 @@
 | Fun2 "ty2" "ty2"
 
 nominal_datatype tys2 =
-  All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
+  All2 xs::"name fset" ty::"ty2" bind (set+) xs in ty
 
 thm tys2.distinct
 thm tys2.induct tys2.strong_induct