--- a/FIXME-TODO	Wed Jan 13 16:23:32 2010 +0100
+++ b/FIXME-TODO	Wed Jan 13 16:39:20 2010 +0100
@@ -4,23 +4,6 @@
 - better lookup mechanism for quotient definition
   (see fixme in quotient_term.ML)
 
-- check needs to be fixed in mk_resp_arg (quotient_term.ML),
-  see test for (_, Const _)
-
-- clever code in quotiet_tacs.ML needs to be turned into
-  boring code
-
-- comment about regularize tactic needs to be adapted
-
-- Check all the places where we do "handle _"
-  (They make code changes very difficult: I sat 1/2
-  a day over a simplification of calculate_inst before
-  I understood things; the reason was that my exceptions
-  where caught by the catch all. There is no problem
-  with throwing and handling exceptions...it just must
-  be clear who throws what and what is thrown.)
-
-
 Higher Priority
 ===============
 
@@ -34,10 +17,6 @@
 - If the constant definition gives the wrong definition
   term, one gets a cryptic message about absrep_fun
 
-- have FSet.thy to have a simple infrastructure for 
-  finite sets (syntax should be \<lbrace> \<rbrace>,
-  look at Set.thy how syntax is been introduced)
-
 - Handle theorems that include Ball/Bex. For this, would 
   it help if we introduced separate Bex and Ball constants 
   for quotienting?
@@ -49,10 +28,6 @@
 Lower Priority
 ==============
 
-- Maybe a quotient_definition should already require
-  a proof of the respectfulness (in this way one
-  already excludes non-sensical definitions)
-
 - accept partial equivalence relations
 
 - think about what happens if things go wrong (like

--- 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

--- a/Quot/quotient_tacs.ML	Wed Jan 13 16:23:32 2010 +0100
+++ b/Quot/quotient_tacs.ML	Wed Jan 13 16:39:20 2010 +0100
@@ -51,16 +51,12 @@
 
 (** solvers for equivp and quotient assumptions **)
 
-(* FIXME / TODO: should this SOLVED' the goal, like with quotient_tac? *)
-(* FIXME / TODO: none of te examples break if added                    *)
 fun equiv_tac ctxt =
   REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
 
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 
-(* FIXME / TODO: test whether DETERM makes any runtime-difference *)
-(* FIXME / TODO: reason: the tactic might back-track over the two alternatives in FIRST' *)
 fun quotient_tac ctxt = SOLVED'
   (REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
@@ -279,8 +275,6 @@
       end
   | _ => K no_tac
 end
-(* TODO: Again, can one specify more concretely        *)
-(* TODO: in terms of R when no_tac should be returned? *)
 
 fun rep_abs_rsp_tac ctxt =
   SUBGOAL (fn (goal, i) =>

--- a/Quot/quotient_typ.ML	Wed Jan 13 16:23:32 2010 +0100
+++ b/Quot/quotient_typ.ML	Wed Jan 13 16:39:20 2010 +0100
@@ -212,7 +212,7 @@
   fun map_check_aux rty warns =
     case rty of
       Type (_, []) => warns
-    | Type (s, _) => if (maps_exists thy s) then warns else s::warns
+    | Type (s, _) => if (maps_defined thy s) then warns else s::warns
     | _ => warns
 
   val warns = map_check_aux rty []