--- a/quotient.ML	Tue Oct 27 11:43:02 2009 +0100
+++ b/quotient.ML	Tue Oct 27 14:14:30 2009 +0100
@@ -1,7 +1,7 @@
 signature QUOTIENT =
 sig
   type maps_info = {mapfun: string, relfun: string}
-  type quotient_info = {qtyp: typ, rtyp: typ, rel: term}
+  type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
   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
   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
@@ -11,8 +11,8 @@
   val maps_update: string -> maps_info -> Proof.context -> Proof.context                           
   val print_quotdata: Proof.context -> unit
   val quotdata_lookup: theory -> quotient_info list
-  val quotdata_update_thy: (typ * typ * term) -> theory -> theory
-  val quotdata_update: (typ * typ * term) -> Proof.context -> Proof.context
+  val quotdata_update_thy: (typ * typ * term * thm) -> theory -> theory
+  val quotdata_update: (typ * typ * term * thm) -> Proof.context -> Proof.context
 end;
 
 structure Quotient: QUOTIENT =
@@ -61,7 +61,7 @@
 
 
 (* info about the quotient types *)
-type quotient_info = {qtyp: typ, rtyp: typ, rel: term}
+type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
 
 structure QuotData = TheoryDataFun
   (type T = quotient_info list
@@ -72,22 +72,24 @@
 
 val quotdata_lookup = QuotData.get
 
-fun quotdata_update_thy (qty, rty, rel) thy = 
-      QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) thy
+fun quotdata_update_thy (qty, rty, rel, equiv_thm) thy = 
+      QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel, equiv_thm = equiv_thm}::ls) thy
 
-fun quotdata_update (qty, rty, rel) ctxt = 
-      ProofContext.theory (quotdata_update_thy (qty, rty, rel)) ctxt
+fun quotdata_update (qty, rty, rel, equiv_thm) ctxt = 
+      ProofContext.theory (quotdata_update_thy (qty, rty, rel, equiv_thm)) ctxt
 
 fun print_quotdata ctxt =
 let
-  fun prt_quot {qtyp, rtyp, rel} = 
+  fun prt_quot {qtyp, rtyp, rel, equiv_thm} = 
       Pretty.block (Library.separate (Pretty.brk 2)
           [Pretty.str ("quotient type:"), 
            Syntax.pretty_typ ctxt qtyp,
            Pretty.str ("raw type:"), 
            Syntax.pretty_typ ctxt rtyp,
            Pretty.str ("relation:"), 
-           Syntax.pretty_term ctxt rel])
+           Syntax.pretty_term ctxt rel,
+           Pretty.str ("equiv. thm:"), 
+           Syntax.pretty_term ctxt (prop_of equiv_thm)])
 in
   QuotData.get (ProofContext.theory_of ctxt)
   |> map prt_quot
@@ -101,7 +103,7 @@
 
 
 
-(* wrappers for define and note *)
+(* wrappers for define, note and theorem_i*)
 fun define (name, mx, rhs) lthy =
 let
   val ((rhs, (_ , thm)), lthy') =
@@ -117,6 +119,13 @@
   (thm', lthy')
 end
 
+fun theorem after_qed goals ctxt =
+let
+  val goals' = map (rpair []) goals
+  fun after_qed' thms = after_qed (the_single thms)
+in 
+  Proof.theorem_i NONE after_qed' [goals'] ctxt
+end
 
 
 (* definition of the quotient type *)
@@ -231,7 +240,7 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* storing the quot-info *)
-  val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2
+  val lthy3 = quotdata_update (abs_ty, rty, rel, equiv_thm) lthy2
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
@@ -281,15 +290,15 @@
   let
     val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   in 
-    (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), [])
+    HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel)
   end
 
   val goals = map (mk_goal o snd) quot_list
               
   fun after_qed thms lthy =
-    fold_map mk_typedef_main (quot_list ~~ (flat thms)) lthy |> snd
+    fold_map mk_typedef_main (quot_list ~~ thms) lthy |> snd
 in
-  Proof.theorem_i NONE after_qed [goals] lthy
+  theorem after_qed goals lthy
 end
 
 val quotspec_parser =