--- a/quotient.ML	Sun Oct 25 01:31:04 2009 +0200
+++ b/quotient.ML	Sun Oct 25 23:44:41 2009 +0100
@@ -7,7 +7,8 @@
   val define: binding * mixfix * term -> local_theory -> (term * thm) * local_theory
   val note: binding * thm -> local_theory -> thm * local_theory
   val maps_lookup: theory -> string -> maps_info option
-  val maps_update: string -> maps_info -> theory -> theory                                  
+  val maps_update_thy: string -> maps_info -> theory -> theory    
+  val maps_update: string -> maps_info -> Proof.context -> Proof.context                           
   val print_quotdata: Proof.context -> unit
   val quotdata_lookup: theory -> quotient_info list
   val quotdata_update_thy: (typ * typ * term) -> theory -> theory
@@ -31,7 +32,32 @@
    fun merge _ = Symtab.merge (K true))
 
 val maps_lookup = Symtab.lookup o MapsData.get
-fun maps_update k v = MapsData.map (Symtab.update (k, v))
+fun maps_update_thy k minfo = MapsData.map (Symtab.update (k, minfo))
+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))
+
+(* attribute to be used in declare statements *)
+fun maps_attribute (ctxt, (tystr, (mapstr, relstr))) = 
+let  
+  val thy = ProofContext.theory_of ctxt
+  val tyname = Sign.intern_type thy tystr
+  val mapname = Sign.intern_const thy mapstr
+  val relname = Sign.intern_const thy relstr
+in
+  maps_attribute_aux tyname {mapfun = mapname, relfun = relname}
+end
+
+val maps_attr_parser = 
+      Args.context -- Scan.lift
+       ((Args.name --| OuterParse.$$$ "=") -- 
+         (OuterParse.$$$ "(" |-- Args.name --| OuterParse.$$$ "," -- 
+           Args.name --| OuterParse.$$$ ")"))
+
+val _ = Context.>> (Context.map_theory
+         (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) 
+           "declaration of map information"))
 
 
 (* info about the quotient types *)
@@ -42,31 +68,35 @@
    val empty = []
    val copy = I
    val extend = I
-   fun merge _ = (op @))
+   fun merge _ = (op @)) (* FIXME: is this the correct merging function for the list? *)
 
 val quotdata_lookup = QuotData.get
 
-fun quotdata_update_thy (qty, rty, rel) = 
-      QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls)
+fun quotdata_update_thy (qty, rty, rel) thy = 
+      QuotData.map (fn ls => {qtyp = qty, rtyp = rty, rel = rel}::ls) thy
 
-fun quotdata_update (qty, rty, rel) = 
-      ProofContext.theory (quotdata_update_thy (qty, rty, rel))
+fun quotdata_update (qty, rty, rel) ctxt = 
+      ProofContext.theory (quotdata_update_thy (qty, rty, rel)) ctxt
 
 fun print_quotdata ctxt =
 let
-  val quots = QuotData.get (ProofContext.theory_of ctxt)
   fun prt_quot {qtyp, rtyp, rel} = 
-      Pretty.block [Pretty.str ("quotient:"), 
-                    Pretty.brk 2, Syntax.pretty_typ ctxt qtyp,
-                    Pretty.brk 2, Syntax.pretty_typ ctxt rtyp,
-                    Pretty.brk 2, Syntax.pretty_term ctxt rel]
+      Pretty.block (Library.separate (Pretty.brk 2)
+          [Pretty.str ("quotient type:"), 
+           Syntax.pretty_typ ctxt qtyp,
+           Pretty.str ("raw type:"), 
+           Syntax.pretty_typ ctxt rtyp,
+           Pretty.str ("relation:"), 
+           Syntax.pretty_term ctxt rel])
 in
-  [Pretty.big_list "quotients:" (map prt_quot quots)]
-  |> Pretty.chunks |> Pretty.writeln
+  QuotData.get (ProofContext.theory_of ctxt)
+  |> map prt_quot
+  |> Pretty.big_list "quotients:" 
+  |> Pretty.writeln
 end
 
 val _ = 
-  OuterSyntax.improper_command "print_quotients" "print quotient types of this theory" 
+  OuterSyntax.improper_command "print_quotients" "print out all quotients" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotdata o Toplevel.context_of)))
 
 
@@ -200,7 +230,6 @@
   val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy2
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
-					      
   (* storing the quot-info *)
   val lthy3 = quotdata_update (abs_ty, rty, rel) lthy2
 
@@ -248,14 +277,14 @@
 
 fun mk_quotient_type quot_list lthy = 
 let
-  fun get_goal (rty, rel) =
+  fun mk_goal (rty, rel) =
   let
     val EQUIV_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
   in 
     (HOLogic.mk_Trueprop (Const (@{const_name EQUIV}, EQUIV_ty) $ rel), [])
   end
 
-  val goals = map (get_goal o snd) quot_list
+  val goals = map (mk_goal o snd) quot_list
               
   fun after_qed thms lthy =
     fold_map mk_typedef_main (quot_list ~~ (flat thms)) lthy |> snd