--- a/Quot/quotient_tacs.ML	Mon Jan 11 20:04:19 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 12 10:59:38 2010 +0100
@@ -260,21 +260,26 @@
     | _ => no_tac
   end)
 
+(* Instantiates and applies 'equals_rsp'. Since the theorem is
+   complex we rely on instantiation to tell us if it applies *)
 fun equals_rsp_tac R ctxt =
 let
-  val ty = domain_type (fastype_of R);
   val thy = ProofContext.theory_of ctxt
-  val thm = Drule.instantiate' 
-               [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)] @{thm equals_rsp}
 in
-  rtac thm THEN' quotient_tac ctxt
+  case try (cterm_of thy) R of (* There can be loose bounds in R *)
+    SOME ctm =>
+      let
+        val ty = domain_type (fastype_of R)
+      in
+        case try (Drule.instantiate' [SOME (ctyp_of thy ty)]
+          [SOME (cterm_of thy R)]) @{thm equals_rsp} of
+          SOME thm => rtac thm THEN' quotient_tac ctxt
+        | NONE => K no_tac
+      end
+  | _ => K no_tac
 end
-(* TODO: Are they raised by instantiate'?              *)
 (* TODO: Again, can one specify more concretely        *)
 (* TODO: in terms of R when no_tac should be returned? *)
-handle THM _  => K no_tac
-     | TYPE _ => K no_tac
-     | TERM _ => K no_tac
 
 fun rep_abs_rsp_tac ctxt = 
   SUBGOAL (fn (goal, i) =>