--- a/quotient_info.ML	Thu Dec 03 11:58:46 2009 +0100
+++ b/quotient_info.ML	Thu Dec 03 12:17:23 2009 +0100
@@ -13,7 +13,7 @@
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
   val quotdata_dest: theory -> quotient_info list
 
-  type qconsts_info = {qconst: term, rconst: term}
+  type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
   val qconsts_lookup: theory -> string -> qconsts_info option
   val qconsts_update_thy: string -> qconsts_info -> theory -> theory    
@@ -118,7 +118,7 @@
 
 
 (* info about quotient constants *)
-type qconsts_info = {qconst: term, rconst: term}
+type qconsts_info = {qconst: term, rconst: term, def: thm}
 
 structure QConstsData = Theory_Data
   (type T = qconsts_info Symtab.table
@@ -126,18 +126,20 @@
    val extend = I
    val merge = Symtab.merge (K true))
 
-fun qconsts_transfer phi {qconst, rconst} =
+fun qconsts_transfer phi {qconst, rconst, def} =
     {qconst = Morphism.term phi qconst,
-     rconst = Morphism.term phi rconst}
+     rconst = Morphism.term phi rconst,
+     def = Morphism.thm phi def}
 
 val qconsts_lookup = Symtab.lookup o QConstsData.get
 
 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
 fun qconsts_update_gen k qcinfo = Context.mapping (qconsts_update_thy k qcinfo) I
 
+(* We don't print the definition *)
 fun print_qconstinfo ctxt =
 let
-  fun prt_qconst {qconst, rconst} = 
+  fun prt_qconst {qconst, rconst, def} =
       Pretty.block (separate (Pretty.brk 1)
           [Syntax.pretty_term ctxt qconst,
            Pretty.str ":=",