diff -r ba7e81531c6d -r d193e2111811 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Fri Jan 01 23:59:32 2010 +0100
+++ b/Quot/quotient_info.ML	Sat Jan 02 23:15:15 2010 +0100
@@ -3,6 +3,7 @@
   exception NotFound
 
   type maps_info = {mapfun: string, relmap: string}
+  val maps_exists: 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,6 +78,11 @@
    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_lookup thy s = 
   case (Symtab.lookup (MapsData.get thy) s) of
     SOME map_fun => map_fun