--- a/Quot/quotient_info.ML	Wed Dec 23 23:53:03 2009 +0100
+++ b/Quot/quotient_info.ML	Thu Dec 24 00:58:50 2009 +0100
@@ -8,12 +8,12 @@
   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
   val print_mapsinfo: Proof.context -> unit
 
-  type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
-  val quotdata_lookup_thy: theory -> string -> quotient_info     (* raises NotFound *)
-  val quotdata_lookup: Proof.context -> string -> quotient_info     (* raises NotFound *)
-  val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
-  val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
-  val quotdata_dest: theory -> quotient_info list
+  type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+  val quotdata_transfer: morphism -> quotdata_info -> quotdata_info
+  val quotdata_lookup: theory -> string -> quotdata_info     (* raises NotFound *)
+  val quotdata_update_thy: string -> quotdata_info -> theory -> theory
+  val quotdata_update_gen: string -> quotdata_info -> Context.generic -> Context.generic
+  val quotdata_dest: theory -> quotdata_info list
   val print_quotinfo: Proof.context -> unit
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
@@ -60,7 +60,7 @@
 fun maps_update k minfo = ProofContext.theory (maps_update_thy k minfo)
 
 fun maps_attribute_aux s minfo = Thm.declaration_attribute 
-  (fn thm => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
+  (fn _ => Context.mapping (maps_update_thy s minfo) (maps_update s minfo))
 
 (* attribute to be used in declare statements *)
 fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = 
@@ -98,36 +98,33 @@
   MapsData.get (ProofContext.theory_of ctxt)
   |> Symtab.dest
   |> map (prt_map)
-  |> Pretty.big_list "maps:" 
+  |> Pretty.big_list "maps for type constructors:" 
   |> Pretty.writeln
 end
 
  
 (* info about quotient types *)
-type quotient_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
+type quotdata_info = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm}
 
 structure QuotData = Theory_Data
-  (type T = quotient_info Symtab.table
+  (type T = quotdata_info Symtab.table
    val empty = Symtab.empty
    val extend = I
    val merge = Symtab.merge (K true)) 
 
-fun quotdata_lookup_thy thy s = 
-  case Symtab.lookup (QuotData.get thy) (Sign.intern_type thy s) of
+fun quotdata_transfer phi {qtyp, rtyp, equiv_rel, equiv_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}
+
+fun quotdata_lookup thy str = 
+  case Symtab.lookup (QuotData.get thy) str of
     SOME qinfo => qinfo
   | NONE => raise NotFound
 
-val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
-
-fun quotdata_update_thy qty_name (qty, rty, equiv_rel, equiv_thm) =
-let
-  val qinfo = {qtyp = qty, rtyp = rty, equiv_rel = equiv_rel, equiv_thm = equiv_thm}
-in
-  QuotData.map (Symtab.update (qty_name, qinfo))
-end
-
-fun quotdata_update qty_name (qty, rty, rel, equiv_thm) = 
-      ProofContext.theory (quotdata_update_thy qty_name (qty, rty, rel, equiv_thm))
+fun quotdata_update_thy str qinfo = QuotData.map (Symtab.update (str, qinfo))
+fun quotdata_update_gen str qinfo = Context.mapping (quotdata_update_thy str qinfo) I
 
 fun quotdata_dest thy =
     map snd (Symtab.dest (QuotData.get thy))
@@ -167,8 +164,8 @@
      rconst = Morphism.term phi rconst,
      def = Morphism.thm phi def}
 
-fun qconsts_update_thy id qcinfo = QConstsData.map (Symtab.update (id, qcinfo))
-fun qconsts_update_gen id qcinfo = Context.mapping (qconsts_update_thy id qcinfo) I
+fun qconsts_update_thy str qcinfo = QConstsData.map (Symtab.update (str, qcinfo))
+fun qconsts_update_gen str qcinfo = Context.mapping (qconsts_update_thy str qcinfo) I
 
 fun qconsts_dest thy =
   map snd (Symtab.dest (QConstsData.get thy))