--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Jul 20 15:42:23 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Jul 20 16:15:33 2011 +0200
@@ -286,9 +286,8 @@
fun rep_abs_rsp_tac ctxt =
SUBGOAL (fn (goal, i) =>
(case try bare_concl goal of
- SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac
- | SOME (rel $ _ $ (rep $ (abs $ _))) =>
- let
+ SOME (rel $ _ $ (rep $ (abs $ _))) =>
+ (let
val thy = Proof_Context.theory_of ctxt;
val (ty_a, ty_b) = dest_funT (fastype_of abs);
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
@@ -300,10 +299,10 @@
| NONE => no_tac)
| NONE => no_tac
end
+ handle TERM _ => no_tac)
| _ => no_tac))
-
(* Injection means to prove that the regularized theorem implies
the abs/rep injected one.