diff -r ba7e81531c6d -r d193e2111811 Quot/quotient_typ.ML
--- a/Quot/quotient_typ.ML	Fri Jan 01 23:59:32 2010 +0100
+++ b/Quot/quotient_typ.ML	Sat Jan 02 23:15:15 2010 +0100
@@ -166,7 +166,7 @@
 end
 
 
-(* sanity checks of the quotient type specifications *)
+(* sanity checks for the quotient type specifications *)
 fun sanity_check ((vs, qty_name, _), (rty, rel)) =
 let
   val rty_tfreesT = map fst (Term.add_tfreesT rty [])
@@ -205,6 +205,24 @@
   if null errs then () else error (cat_lines errs)
 end
 
+(* check for existence of map functions *)
+fun map_check ctxt (_, (rty, _)) =
+let
+  val thy = ProofContext.theory_of ctxt
+
+  fun map_check_aux rty warns =
+    case rty of
+      Type (_, []) => warns
+    | Type (s, _) => if (maps_exists thy s) then warns else s::warns
+    | _ => warns
+
+  val warns = map_check_aux rty []
+in
+  if null warns then () 
+  else warning ("No map function defined for " ^ (commas warns) ^ 
+                ". This will cause problems later on.")
+end
+
 
 (******************************)
 (* interface and syntax setup *)
@@ -225,6 +243,7 @@
 let
   (* sanity check *)  
   val _ = map sanity_check quot_list 
+  val _ = map (map_check lthy) quot_list
 
   fun mk_goal (rty, rel) =
   let