--- a/quotient.ML	Mon Oct 12 23:39:14 2009 +0200
+++ b/quotient.ML	Tue Oct 13 00:02:22 2009 +0200
@@ -178,6 +178,7 @@
   Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy
 end
 
+(* FIXME: allow more than one type definition *)
 val quottype_parser = 
     P.short_ident -- P.opt_infix -- 
        (P.$$$ "=" |-- P.typ) -- 
@@ -196,7 +197,7 @@
 
 val _ = 
     OuterSyntax.local_theory_to_proof "quotient" 
-      "quotient type definition (requires equivalence proof)"
+      "quotient type definitions (requires equivalence proofs)"
          OuterKeyword.thy_goal (quottype_parser >> mk_typedef_cmd)	     
 
 end; (* local *)