# HG changeset patch # User wenzelm # Date 1323803411 -3600 # Node ID 14bf7ca4ef3a1b34c50ff998e4e4cfd2825d2477 # Parent 9c232d370244c757eadf70094677f9e827d2b321 comment; diff -r 9c232d370244 -r 14bf7ca4ef3a src/HOL/Tools/Quotient/quotient_type.ML --- a/src/HOL/Tools/Quotient/quotient_type.ML Tue Dec 13 16:53:28 2011 +0100 +++ b/src/HOL/Tools/Quotient/quotient_type.ML Tue Dec 13 20:10:11 2011 +0100 @@ -277,6 +277,7 @@ val quotspec_parser = Parse.and_list1 ((Parse.type_args -- Parse.binding) -- + (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *) Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) -- (Parse.$$$ "/" |-- (partial -- Parse.term)) -- Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding)))