# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1311171333 -7200
# Node ID aa04d1e1e2cc2999894b63e5442c4c283ea88849
# Parent  2108763f298ddee1cdadd577cfc09f3f6deb381c# Parent  6cc1875cf35da11b0d8c31e9eea33712475e723e
merge

diff -r 6cc1875cf35d -r aa04d1e1e2cc src/HOL/Tools/Quotient/quotient_tacs.ML
--- 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.