diff -r df962ca75ffa -r fe2529a9f250 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 14 13:59:08 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 14 14:24:08 2009 +0100
@@ -431,7 +431,7 @@
 
 
 (* 0. preliminary simplification step according to *)
-thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *)
+thm ball_reg_eqv bex_reg_eqv (* babs_reg_eqv is of no use *)
     ball_reg_eqv_range bex_reg_eqv_range
 (* 1. eliminating simple Ball/Bex instances*)
 thm ball_reg_right bex_reg_left
@@ -706,19 +706,22 @@
 thm rep_abs_rsp
 
 ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
+
 fun rep_abs_rsp_tac ctxt = 
   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' SOLVE o (quotient_tac ctxt)) i
+           (rtac inst_thm THEN' SOLVES' (quotient_tac ctxt)) i
          end
+         handle THM _ => no_tac | TYPE _ => no_tac)
     | _ => no_tac)
 *}
 
@@ -1060,8 +1063,6 @@
 section {* Automatic Proofs *}
 
 ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
-
 (* prints warning, if goal is unsolved *)
 fun WARN (tac, msg) i st =
  case Seq.pull ((SOLVES' tac) i st) of