--- a/QuotMain.thy	Sun Oct 18 10:34:53 2009 +0200
+++ b/QuotMain.thy	Tue Oct 20 00:12:05 2009 +0200
@@ -147,7 +147,15 @@
 
 use "quotient.ML"
 
-term EQUIV
+(* 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"}}
+*}
+
+
+ML {* maps_lookup @{theory} @{type_name list} *}
 
 ML {*
 val no_vars = Thm.rule_attribute (fn context => fn th =>
@@ -225,33 +233,6 @@
 
 section {* lifting of constants *}
 
-text {* information about map-functions for type-constructor *}
-ML {*
-type typ_info = {mapfun: string, relfun: string}
-
-local
-  structure Data = TheoryDataFun
-  (type T = typ_info Symtab.table
-   val empty = Symtab.empty
-   val copy = I
-   val extend = I
-   fun merge _ = Symtab.merge (K true))
-in
-  val lookup = Symtab.lookup o Data.get
-  fun update k v = Data.map (Symtab.update (k, v))
-end
-*}
-
-(* mapfuns for some standard types *)
-setup {*
-  update @{type_name "list"} {mapfun = @{const_name "map"},      relfun = @{const_name "LIST_REL"}} #>
-  update @{type_name "*"}    {mapfun = @{const_name "prod_fun"}, relfun = @{const_name "prod_rel"}} #>
-  update @{type_name "fun"}  {mapfun = @{const_name "fun_map"},  relfun = @{const_name "FUN_REL"}}
-*}
-
-
-ML {* lookup @{theory} @{type_name list} *}
-
 ML {*
 (* calculates the aggregate abs and rep functions for a given type; 
    repF is for constants' arguments; absF is for constants;
@@ -275,7 +256,7 @@
     val nty = Type (s, ntys)
     val ftys = map (op -->) tys
   in
-   (case (lookup (ProofContext.theory_of lthy) s) of
+   (case (maps_lookup (ProofContext.theory_of lthy) s) of
       SOME info => (list_comb (Const (#mapfun info, ftys ---> (oty --> nty)), fs), (oty, nty))
     | NONE      => raise ERROR ("no map association for type " ^ s))
   end
@@ -1007,7 +988,7 @@
               val ty_out = ty --> ty --> @{typ bool};
               val tys_out = tys_rel ---> ty_out;
             in
-            (case (lookup (ProofContext.theory_of lthy) s) of
+            (case (maps_lookup (ProofContext.theory_of lthy) s) of
                SOME (info) => list_comb (Const (#relfun info, tys_out), map (fn ty => tyRel ty rty rel lthy) tys)
              | NONE  => HOLogic.eq_const ty
             )