# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1255384942 -7200
# Node ID c3d27aada58948423def2f107e8edc975dfddc3c
# Parent  c8d58e2cda58e691658016e2ce2baaf92d3236e2
tuned

diff -r c8d58e2cda58 -r c3d27aada589 quotient.ML
--- 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 *)