diff -r adf22ee09738 -r 0911cb7bf696 Nominal/Nominal2.thy --- 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