--- a/Tutorial/Tutorial6.thy	Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial6.thy	Mon Mar 05 16:27:28 2012 +0000
@@ -17,7 +17,7 @@
   Var "name"
 | Fun "ty" "ty" (infixr "\<rightarrow>" 100)
 and tys =
-  All as::"name fset" ty::"ty" bind (set+) as in ty ("All _. _" [100, 100] 100)
+  All as::"name fset" ty::"ty" binds (set+) as in ty ("All _. _" [100, 100] 100)
 
 
 text {* Some alpha-equivalences *}