--- a/QuotMain.thy	Sat Oct 17 16:06:54 2009 +0200
+++ b/QuotMain.thy	Sun Oct 18 00:52:10 2009 +0200
@@ -3,6 +3,7 @@
 uses ("quotient.ML")
 begin
 
+
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -141,6 +142,7 @@
 
 end
 
+
 section {* type definition for the quotient type *}
 
 use "quotient.ML"
@@ -250,7 +252,6 @@
 
 ML {* lookup @{theory} @{type_name list} *}
 
-
 ML {*
 (* calculates the aggregate abs and rep functions for a given type; 
    repF is for constants' arguments; absF is for constants;

--- a/quotient.ML	Sat Oct 17 16:06:54 2009 +0200
+++ b/quotient.ML	Sun Oct 18 00:52:10 2009 +0200
@@ -1,5 +1,10 @@
+signature QUOTIENT =
+sig
+  val mk_quotient_type: ((binding * mixfix) * (typ * term)) list -> Proof.context -> Proof.state
+  val mk_quotient_type_cmd: (((bstring * mixfix) * string) * string) list -> Proof.context -> Proof.state
+end;
 
-structure Quotient =
+structure Quotient: QUOTIENT =
 struct
 
 (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
@@ -94,7 +99,7 @@
 end
 
 (* main function for constructing the quotient type *)
-fun mk_typedef_main (qty_name, mx, rel, rty, equiv_thm) lthy =
+fun mk_typedef_main (((qty_name, mx), (rty, rel)), equiv_thm) lthy =
 let
   (* generates typedef *)
   val ((_, typedef_info), lthy1) = typedef_make (qty_name, mx, rel, rty) lthy
@@ -160,37 +165,55 @@
       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 end
 
-(* syntax setup *)
-local structure P = OuterParse in
+(* interface and syntax setup *)
 
-fun mk_typedef (qty_name, mx, rty, rel_trm) lthy = 
+(* the ML-interface takes a list of 4-tuples consisting of  *)
+(*                                                          *)
+(* - the name of the quotient type                          *)
+(* - its mixfix annotation                                  *)
+(* - the type to be quotient                                *)
+(* - the relation according to which the type is quotient   *)
+  
+fun mk_quotient_type quot_list lthy = 
 let
-  val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
-  val EQUIV_goal = HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel_trm)
-		    
+  fun get_goal (rty, rel) =
+  let
+    val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
+  in 
+    (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), [])
+  end
+
+  val goals = map (get_goal o snd) quot_list
+              
   fun after_qed thms lthy =
   let
-    val thm = the_single (flat thms)
+    val thms' = flat thms
   in
-    mk_typedef_main (Binding.name qty_name, mx, rel_trm, rty, thm) lthy |> snd   
+    fold_map mk_typedef_main (quot_list ~~ thms') lthy |> snd
   end
 in
-  Proof.theorem_i NONE after_qed [[(EQUIV_goal, [])]] lthy
+  Proof.theorem_i NONE after_qed [goals] lthy
 end
 
-(* FIXME: allow more than one type definition *)
-val quottype_parser = 
-    P.short_ident -- P.opt_infix -- 
-       (P.$$$ "=" |-- P.typ) -- 
-         (P.$$$ "/" |-- P.term)
+val quotspec_parser = 
+    OuterParse.and_list1
+     (OuterParse.short_ident -- OuterParse.opt_infix -- 
+       (OuterParse.$$$ "=" |-- OuterParse.typ) -- 
+         (OuterParse.$$$ "/" |-- OuterParse.term))
            
-fun mk_typedef_cmd (((qstr, mx), rstr), rel_str) lthy = 
+fun mk_quotient_type_cmd spec lthy = 
 let
-  val rty = Syntax.parse_typ lthy rstr
-  val rel_trm = Syntax.parse_term lthy rel_str
-                |> Syntax.check_term lthy
+  fun parse_spec (((qty_str, mx), rty_str), rel_str) =
+  let
+    val qty_name = Binding.name qty_str
+    val rty = Syntax.parse_typ lthy rty_str
+    val rel = Syntax.parse_term lthy rel_str
+              |> Syntax.check_term lthy
+  in
+     ((qty_name, mx), (rty, rel))
+  end
 in
-  mk_typedef (qstr, mx, rty, rel_trm) lthy  
+  mk_quotient_type (map parse_spec spec) lthy
 end
 
 val _ = OuterKeyword.keyword "/"
@@ -198,9 +221,7 @@
 val _ = 
     OuterSyntax.local_theory_to_proof "quotient" 
       "quotient type definitions (requires equivalence proofs)"
-         OuterKeyword.thy_goal (quottype_parser >> mk_typedef_cmd)	     
-
-end; (* local *)
+         OuterKeyword.thy_goal (quotspec_parser >> mk_quotient_type_cmd)
 
 end; (* structure *)