Nominal/Nominal2.thy
changeset 2634 3ce1089cdbf3
parent 2633 d1d09177ec89
child 2639 a8fc346deda3
equal deleted inserted replaced
2633:d1d09177ec89 2634:3ce1089cdbf3
   772 
   772 
   773 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
   773 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
   774 
   774 
   775 val bind_mode = P.$$$ "bind" |--
   775 val bind_mode = P.$$$ "bind" |--
   776   S.optional (Args.parens 
   776   S.optional (Args.parens 
   777     (Args.$$$ "list" >> K Lst || Args.$$$ "set" >> K Set || Args.$$$ "res" >> K Res)) Lst
   777     (Args.$$$ "list" >> K Lst || (Args.$$$ "set" -- Args.$$$ "+") >> K Res || Args.$$$ "set" >> K Set)) Lst
   778 
   778 
   779 val bind_clauses = 
   779 val bind_clauses = 
   780   P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple)
   780   P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple)
   781 
   781 
   782 val cnstr_parser =
   782 val cnstr_parser =