1.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 23 14:17:29 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Mar 23 14:18:43 2012 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
     1.5    val print_abs_rep: Proof.context -> unit
     1.6    
     1.7 -  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
     1.8 +  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
     1.9    val transform_quotients: morphism -> quotients -> quotients
    1.10    val lookup_quotients: Proof.context -> string -> quotients option
    1.11    val lookup_quotients_global: theory -> string -> quotients option
    1.12 @@ -125,7 +125,7 @@
    1.13    end
    1.14  
    1.15  (* info about quotient types *)
    1.16 -type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
    1.17 +type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
    1.18  
    1.19  structure Quotients = Generic_Data
    1.20  (
    1.21 @@ -135,11 +135,12 @@
    1.22    fun merge data = Symtab.merge (K true) data
    1.23  )
    1.24  
    1.25 -fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm} =
    1.26 +fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
    1.27    {qtyp = Morphism.typ phi qtyp,
    1.28     rtyp = Morphism.typ phi rtyp,
    1.29     equiv_rel = Morphism.term phi equiv_rel,
    1.30 -   equiv_thm = Morphism.thm phi equiv_thm}
    1.31 +   equiv_thm = Morphism.thm phi equiv_thm,
    1.32 +   quot_thm = Morphism.thm phi quot_thm}
    1.33  
    1.34  val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
    1.35  val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
    1.36 @@ -151,7 +152,7 @@
    1.37  
    1.38  fun print_quotients ctxt =
    1.39    let
    1.40 -    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm} =
    1.41 +    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
    1.42        Pretty.block (separate (Pretty.brk 2)
    1.43         [Pretty.str "quotient type:",
    1.44          Syntax.pretty_typ ctxt qtyp,
    1.45 @@ -160,7 +161,9 @@
    1.46          Pretty.str "relation:",
    1.47          Syntax.pretty_term ctxt equiv_rel,
    1.48          Pretty.str "equiv. thm:",
    1.49 -        Syntax.pretty_term ctxt (prop_of equiv_thm)])
    1.50 +        Syntax.pretty_term ctxt (prop_of equiv_thm),
    1.51 +        Pretty.str "quot. thm:",
    1.52 +        Syntax.pretty_term ctxt (prop_of quot_thm)])
    1.53    in
    1.54      map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
    1.55      |> Pretty.big_list "quotients:"