diff -r 9a0a0b92e8fe -r b89707cd030f Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Jan 12 12:14:33 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 12 15:48:46 2010 +0100
@@ -281,20 +281,22 @@
 (* TODO: Again, can one specify more concretely        *)
 (* TODO: in terms of R when no_tac should be returned? *)
 
-fun rep_abs_rsp_tac ctxt = 
+fun rep_abs_rsp_tac ctxt =
   SUBGOAL (fn (goal, i) =>
-    case (bare_concl goal) of 
-      (rel $ _ $ (rep $ (abs $ _))) =>
-        (let
-           val thy = ProofContext.theory_of ctxt;
-           val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
-           val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
-           val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
-           val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
-         in
-           (rtac inst_thm THEN' quotient_tac ctxt) i
-         end
-         handle THM _ => no_tac | TYPE _ => no_tac) (* TODO: same here *)
+    case (try bare_concl goal) of
+      SOME (rel $ _ $ (rep $ (abs $ _))) =>
+        let
+          val thy = ProofContext.theory_of ctxt;
+          val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+          val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
+        in
+          case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
+            SOME t_inst =>
+              (case try (Drule.instantiate' ty_inst t_inst) @{thm rep_abs_rsp} of
+                SOME inst_thm => (rtac inst_thm THEN' quotient_tac ctxt) i
+              | NONE => no_tac)
+          | NONE => no_tac
+        end
     | _ => no_tac)