diff -r 116c7a30e0a2 -r f4e8e5df7468 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Mon Jan 11 15:58:38 2010 +0100
+++ b/Quot/quotient_tacs.ML	Mon Jan 11 20:03:43 2010 +0100
@@ -264,14 +264,17 @@
 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
-  case try (Drule.instantiate' [SOME (ctyp_of thy ty)] [SOME (cterm_of thy R)])
-    @{thm equals_rsp} of
-    NONE => K no_tac
-  | SOME thm => rtac thm THEN' quotient_tac ctxt
+  rtac thm THEN' quotient_tac ctxt
 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) =>