--- a/quotient_info.ML	Fri Nov 13 19:32:12 2009 +0100
+++ b/quotient_info.ML	Wed Nov 18 23:52:48 2009 +0100
@@ -17,9 +17,10 @@
   val lookup_qenv: ((typ * typ) -> bool) -> qenv -> typ -> (typ * typ) option
 
   type qconsts_info = {qconst: term, rconst: term}
+  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    
-  val qconsts_update: string -> qconsts_info -> Proof.context -> Proof.context 
+  val qconsts_update_generic: string -> qconsts_info -> Context.generic -> Context.generic 
   val print_qconstinfo: Proof.context -> unit
 end;
 
@@ -137,17 +138,22 @@
    val extend = I
    val merge = Symtab.merge (K true))
 
+fun qconsts_transfer phi {qconst, rconst} =
+    {qconst = Morphism.term phi qconst,
+     rconst = Morphism.term phi rconst}
+
 val qconsts_lookup = Symtab.lookup o QConstsData.get
 
 fun qconsts_update_thy k qcinfo = QConstsData.map (Symtab.update (k, qcinfo))
-fun qconsts_update k qcinfo = ProofContext.theory (qconsts_update_thy k qcinfo)
+fun qconsts_update_generic k qcinfo = 
+      Context.mapping (qconsts_update_thy k qcinfo) I
 
 fun print_qconstinfo ctxt =
 let
   fun prt_qconst {qconst, rconst} = 
-      Pretty.block (Library.separate (Pretty.brk 2)
+      Pretty.block (separate (Pretty.brk 1)
           [Syntax.pretty_term ctxt qconst,
-           Pretty.str (" := "),
+           Pretty.str ":=",
            Syntax.pretty_term ctxt rconst])
 in
   QConstsData.get (ProofContext.theory_of ctxt)