--- a/Nominal/Nominal2.thy	Fri Dec 31 13:31:39 2010 +0000
+++ b/Nominal/Nominal2.thy	Fri Dec 31 15:37:04 2010 +0000
@@ -774,7 +774,7 @@
 
 val bind_mode = P.$$$ "bind" |--
   S.optional (Args.parens 
-    (Args.$$$ "list" >> K Lst || Args.$$$ "set" >> K Set || Args.$$$ "res" >> K Res)) Lst
+    (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst
 
 val bind_clauses = 
   P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple)