src/HOL/Tools/Quotient/quotient_tacs.ML

         => rtac @{thm bex1_rel_rsp} THEN' quotient_tac ctxt
 
   | (_ $
       (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
       (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
-        => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+        => rtac @{thm babs_rsp} THEN' quotient_tac ctxt
 
   | Const (@{const_name HOL.eq},_) $ (R $ _ $ _) $ (_ $ _ $ _) =>
      (rtac @{thm refl} ORELSE'
       (equals_rsp_tac R ctxt THEN' RANGE [
          quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))