--- a/Nominal/Ex/Ex1.thy	Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Ex/Ex1.thy	Tue Jul 05 18:42:34 2011 +0200
@@ -10,10 +10,10 @@
 
 nominal_datatype foo =
   Foo0 "name"
-| Foo1 b::"bar" f::"foo" bind (set) "bv b" in f
+| Foo1 b::"bar" f::"foo" binds (set) "bv b" in f
 and bar =
   Bar0 "name"
-| Bar1 "name" s::"name" b::"bar" bind (set) s in b
+| Bar1 "name" s::"name" b::"bar" binds (set) s in b
 binder
   bv
 where