--- a/Quot/QuotMain.thy	Mon Dec 07 14:14:07 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 14:35:45 2009 +0100
@@ -1,5 +1,5 @@
 theory QuotMain
-imports QuotScript QuotList QuotProd Prove
+imports QuotScript QuotProd Prove
 uses ("quotient_info.ML")
      ("quotient.ML")
      ("quotient_def.ML")
@@ -142,24 +142,24 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 
-declare [[map list = (map, list_rel)]]
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
+(* FIXME: This should throw an exception:
+declare [[map "option" = (bla, blu)]]
+*)
 
 (* identity quotient is not here as it has to be applied first *)
 lemmas [quotient_thm] =
-  fun_quotient list_quotient prod_quotient
+  fun_quotient prod_quotient
 
 lemmas [quotient_rsp] =
-  quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp
+  quot_rel_rsp pair_rsp
 
 (* fun_map is not here since equivp is not true *)
 (* TODO: option, ... *)
 lemmas [quotient_equiv] =
-  identity_equivp list_equivp prod_equivp
+  identity_equivp prod_equivp
 
-
-ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
 ML {* maps_lookup @{theory} "fun" *}
 
@@ -217,21 +217,16 @@
 
 section {* infrastructure about id *}
 
+(* TODO: think where should this be *)
 lemma prod_fun_id: "prod_fun id id \<equiv> id"
   by (rule eq_reflection) (simp add: prod_fun_def)
 
-lemma map_id: "map id \<equiv> id"
-  apply (rule eq_reflection)
-  apply (rule ext)
-  apply (rule_tac list="x" in list.induct)
-  apply (simp_all)
-  done
-
+(* FIXME: make it a list and add map_id to it *)
 lemmas id_simps =
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection,symmetric]
-  prod_fun_id map_id
+  prod_fun_id
 
 ML {*
 fun simp_ids thm =