--- a/Quot/QuotMain.thy	Thu Dec 10 05:02:34 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 05:11:53 2009 +0100
@@ -749,13 +749,16 @@
 ML {*
 fun equals_rsp_tac R ctxt =
   let
-    val t = domain_type (fastype_of R);
+    val ty = domain_type (fastype_of R);
     val thy = ProofContext.theory_of ctxt
-    val thm = Drule.instantiate' [SOME (ctyp_of thy t)] [SOME (cterm_of thy R)] @{thm equals_rsp}
+    val thm = Drule.instantiate' 
+                 [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp}
   in
-    rtac thm THEN' RANGE [quotient_tac ctxt]
+    rtac thm THEN' quotient_tac ctxt
   end
-  handle THM _ => K no_tac | TYPE _ => K no_tac | TERM _ => K no_tac
+  handle THM _  => K no_tac  
+       | TYPE _ => K no_tac    
+       | TERM _ => K no_tac
 *}
 
 ML {*