--- a/Quot/Examples/AbsRepTest.thy	Wed Dec 23 23:53:03 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Thu Dec 24 00:58:50 2009 +0100
@@ -2,6 +2,8 @@
 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List
 begin
 
+print_maps
+
 quotient_type 
   fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 
   apply(rule equivpI)

--- 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))

--- a/Quot/quotient_term.ML	Wed Dec 23 23:53:03 2009 +0100
+++ b/Quot/quotient_term.ML	Thu Dec 24 00:58:50 2009 +0100
@@ -154,7 +154,7 @@
        else 
          let
            val exc = LIFT_MATCH ("mk_resp_arg (no quotient found for type " ^ s ^ ")") 
-           val equiv_rel = #equiv_rel (quotdata_lookup_thy thy s') handle NotFound => raise exc
+           val equiv_rel = #equiv_rel (quotdata_lookup thy s') handle NotFound => raise exc
            (* FIXME: check in this case that the rty and qty *)
            (* FIXME: correspond to each other *)
 

--- a/Quot/quotient_typ.ML	Wed Dec 23 23:53:03 2009 +0100
+++ b/Quot/quotient_typ.ML	Thu Dec 24 00:58:50 2009 +0100
@@ -155,11 +155,12 @@
   val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
 
   (* storing the quot-info *)
-  val lthy4 = quotdata_update qty_full_name 
-               (Logic.varifyT Abs_ty, Logic.varifyT rty, map_types Logic.varifyT rel, equiv_thm) lthy3  
   (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *)
-  (* FIXME: The relation can be any term, that later maybe needs to be given *)
-  (* FIXME: a different type (in regularize_trm); how should this be done?   *)
+  fun qinfo phi = quotdata_transfer phi
+                    {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, 
+                     equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm}
+  val lthy4 = Local_Theory.declaration true
+                (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3  
 in
   lthy4
   |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])