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