--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Feb 14 20:08:59 2012 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Tue Feb 14 20:09:35 2012 +0100
@@ -364,7 +364,7 @@
| (_ $
(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'