src/HOL/Tools/Quotient/quotient_type.ML
changeset 45835 14bf7ca4ef3a
parent 45795 2d8949268303
child 46727 0162a0d284ac
equal deleted inserted replaced
45834:9c232d370244 45835:14bf7ca4ef3a
   275 val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
   275 val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
   276 
   276 
   277 val quotspec_parser =
   277 val quotspec_parser =
   278   Parse.and_list1
   278   Parse.and_list1
   279     ((Parse.type_args -- Parse.binding) --
   279     ((Parse.type_args -- Parse.binding) --
       
   280       (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
   280       Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
   281       Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
   281         (Parse.$$$ "/" |-- (partial -- Parse.term))  --
   282         (Parse.$$$ "/" |-- (partial -- Parse.term))  --
   282         Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
   283         Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))
   283 
   284 
   284 val _ = Keyword.keyword "/"
   285 val _ = Keyword.keyword "/"