src/HOL/Tools/Quotient/quotient_info.ML

   val lookup_abs_rep: Proof.context -> string -> abs_rep option
   val lookup_abs_rep_global: theory -> string -> abs_rep option
   val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
   val print_abs_rep: Proof.context -> unit
   
-  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
   val transform_quotients: morphism -> quotients -> quotients
   val lookup_quotients: Proof.context -> string -> quotients option
   val lookup_quotients_global: theory -> string -> quotients option
   val update_quotients: string -> quotients -> Context.generic -> Context.generic
   val dest_quotients: Proof.context -> quotients list

     |> Pretty.big_list "abs/rep terms:"
     |> Pretty.writeln
   end
 
 (* info about quotient types *)
-type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
 
 structure Quotients = Generic_Data
 (
   type T = quotients Symtab.table
   val empty = Symtab.empty
   val extend = I
   fun merge data = Symtab.merge (K true) data
 )
 
-fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} =
+fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
   {qtyp = Morphism.typ phi qtyp,
    rtyp = Morphism.typ phi rtyp,
    equiv_rel = Morphism.term phi equiv_rel,
-   equiv_thm = Morphism.thm phi equiv_thm}
+   equiv_thm = Morphism.thm phi equiv_thm,
+   quot_thm = Morphism.thm phi quot_thm}
 
 val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
 val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
 
 fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))

 fun dest_quotients ctxt =  (* FIXME slightly expensive way to retrieve data *)
   map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
 
 fun print_quotients ctxt =
   let
-    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
+    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
       Pretty.block (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 equiv_rel,
         Pretty.str "equiv. thm:",
-        Syntax.pretty_term ctxt (prop_of equiv_thm)])
+        Syntax.pretty_term ctxt (prop_of equiv_thm),
+        Pretty.str "quot. thm:",
+        Syntax.pretty_term ctxt (prop_of quot_thm)])
   in
     map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
     |> Pretty.big_list "quotients:"
     |> Pretty.writeln
   end