# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260418313 -3600
# Node ID d5c888ec56c79cb486d9449f51ad3837db6d2c9b
# Parent  44fe82707e0e9ce77940c55dcb36f7944463da89
more tuning

diff -r 44fe82707e0e -r d5c888ec56c7 Quot/QuotMain.thy
--- 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 {*