Nominal/Nominal2.thy
changeset 2950 0911cb7bf696
parent 2943 09834ba7ce59
child 2957 01ff621599bc
--- 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