--- a/Quot/quotient_info.ML	Wed Jan 13 16:23:32 2010 +0100
+++ b/Quot/quotient_info.ML	Wed Jan 13 16:39:20 2010 +0100
@@ -3,7 +3,7 @@
   exception NotFound
 
   type maps_info = {mapfun: string, relmap: string}
-  val maps_exists: theory -> string -> bool
+  val maps_defined: theory -> string -> bool
   val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
@@ -77,10 +77,8 @@
    val extend = I
    val merge = Symtab.merge (K true))
 
-fun maps_exists thy s = 
-  case (Symtab.lookup (MapsData.get thy) s) of
-    SOME _ => true
-  | NONE => false
+fun maps_defined thy s = 
+  Symtab.defined (MapsData.get thy) s
 
 fun maps_lookup thy s = 
   case (Symtab.lookup (MapsData.get thy) s) of
@@ -101,8 +99,8 @@
   val mapname = Sign.intern_const thy mapstr
   val relname = Sign.intern_const thy relstr
 
-  fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt)
-  val _ =  map sanity_check [mapname, relname]
+  fun sanity_check s = (Const (s, dummyT) |> Syntax.check_term ctxt; ())
+  val _ =  List.app sanity_check [mapname, relname]
 in
   maps_attribute_aux tyname {mapfun = mapname, relmap = relname}
 end