--- a/QuotMain.thy	Sun Oct 25 01:31:04 2009 +0200
+++ b/QuotMain.thy	Sun Oct 25 23:44:41 2009 +0100
@@ -3,17 +3,6 @@
 uses ("quotient.ML")
 begin
 
-definition 
-  EQ_TRUE 
-where
-  "EQ_TRUE X \<equiv> (X = True)"
-
-lemma test: "EQ_TRUE ?X"
-  unfolding EQ_TRUE_def
-  by (rule refl)
-
-thm test
-
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -155,14 +144,17 @@
 
 section {* type definition for the quotient type *}
 
+ML {* Toplevel.theory *}
+
 use "quotient.ML"
 
-(* mapfuns for some standard types *)
-setup {*
-  maps_update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
-  maps_update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
-  maps_update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
-*}
+declare [[map list = (map, LIST_REL)]]
+declare [[map * = (prod_fun, prod_rel)]]
+declare [[map "fun" = (fun_map, FUN_REL)]]
+
+ML {* maps_lookup @{theory} "List.list" *}
+ML {* maps_lookup @{theory} "*" *}
+ML {* maps_lookup @{theory} "fun" *}
 
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -175,6 +167,10 @@
 section {* lifting of constants *}
 
 ML {*
+
+*}
+
+ML {*
 (* calculates the aggregate abs and rep functions for a given type; 
    repF is for constants' arguments; absF is for constants;
    function types need to be treated specially, since repF and absF

--- a/QuotTest.thy	Sun Oct 25 01:31:04 2009 +0200
+++ b/QuotTest.thy	Sun Oct 25 23:44:41 2009 +0100
@@ -13,13 +13,13 @@
 where
   r_eq: "EQUIV RR"
 
-ML {* print_quotdata @{context} *}
+print_quotients
 
 quotient qtrm = trm / "RR"
   apply(rule r_eq)
   done
 
-ML {* print_quotdata @{context} *}
+print_quotients
 
 typ qtrm
 term Rep_qtrm
@@ -51,6 +51,7 @@
   apply(rule r_eq')
   done
 
+print_quotients
 print_theorems
 
 term ABS_qtrm'
@@ -72,6 +73,13 @@
 quotient qt = "t" / "Rt"
   by (rule t_eq)
 
+print_quotients
+
+ML {*
+Toplevel.context_of;
+Toplevel.keep
+*}
+
 ML {*
   get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"}
   |> fst
@@ -130,6 +138,7 @@
   apply(rule t_eq')
   done
 
+print_quotients
 print_theorems
 
 local_setup {*

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