--- 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)))