changeset 2634 | 3ce1089cdbf3 |
parent 2633 | d1d09177ec89 |
child 2639 | a8fc346deda3 |
--- 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)