--- a/Quot/QuotMain.thy	Mon Dec 14 10:19:27 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 14 13:58:51 2009 +0100
@@ -411,7 +411,7 @@
 
 ML {*
 fun quotient_tac ctxt =
-  DETERM o REPEAT_ALL_NEW (FIRST'
+  REPEAT_ALL_NEW (DETERM o FIRST'
     [rtac @{thm identity_quotient},
      resolve_tac (quotient_rules_get ctxt)])
 
@@ -710,18 +710,15 @@
   SUBGOAL (fn (goal, i) =>
     case (bare_concl goal) of 
       (rel $ _ $ (rep $ (abs $ _))) =>
-        (let
+         let
            val thy = ProofContext.theory_of ctxt;
            val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
            val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
            val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
            val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
          in
-           (rtac inst_thm THEN' quotient_tac ctxt) i
+           (rtac inst_thm THEN' SOLVE o (quotient_tac ctxt)) i
          end
-         handle _ => no_tac) (* FIXME / TODO what is the catch for ? Should go away, no? *)
-(* The catch was for an error of solve_quotient_assum. You replaced it by quotient_tac
-   so I suppose it is equivalent to a "SOLVES" around quotient_tac. *)
     | _ => no_tac)
 *}