diff -r f7602653dddd -r 3a8978c335f0 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 24 16:15:58 2009 +0200
+++ b/QuotMain.thy	Sat Oct 24 16:15:33 2009 +0200
@@ -158,6 +158,12 @@
 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"}}
+*}
+
 
 ML {* quotdata_lookup @{theory} *}
 setup {* quotdata_update_thy (@{typ nat}, @{typ bool}, @{term "True"})*}