# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1311171289 -7200
# Node ID 2108763f298ddee1cdadd577cfc09f3f6deb381c
# Parent  c92df8144681537fa810ccb56c23fdcc228e02b7
Quotient Package: handle Bound variables in rep_abs_rsp_tac not only at top-level of the goal

diff -r c92df8144681 -r 2108763f298d src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Jul 20 13:29:54 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Jul 20 16:14:49 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.