--- a/Nominal/Nominal2.thy Tue Jul 05 18:01:54 2011 +0200
+++ b/Nominal/Nominal2.thy Tue Jul 05 18:42:34 2011 +0200
@@ -679,13 +679,13 @@
fun tuple3 ((x, y), (z, u)) = (x, y, z, u)
in
-val _ = Keyword.keyword "bind"
+val _ = Keyword.keyword "binds"
val opt_name = Scan.option (P.binding --| Args.colon)
val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
-val bind_mode = P.$$$ "bind" |--
+val bind_mode = P.$$$ "binds" |--
S.optional (Args.parens
(Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst