1.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Jul 20 13:29:54 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Wed Jul 20 16:14:49 2011 +0200
     1.3 @@ -286,9 +286,8 @@
     1.4  fun rep_abs_rsp_tac ctxt =
     1.5    SUBGOAL (fn (goal, i) =>
     1.6      (case try bare_concl goal of
     1.7 -      SOME (rel $ _ $ (rep $ (Bound _ $ _))) => no_tac
     1.8 -    | SOME (rel $ _ $ (rep $ (abs $ _))) =>
     1.9 -        let
    1.10 +      SOME (rel $ _ $ (rep $ (abs $ _))) =>
    1.11 +        (let
    1.12            val thy = Proof_Context.theory_of ctxt;
    1.13            val (ty_a, ty_b) = dest_funT (fastype_of abs);
    1.14            val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
    1.15 @@ -300,10 +299,10 @@
    1.16                | NONE => no_tac)
    1.17            | NONE => no_tac
    1.18          end
    1.19 +        handle TERM _ => no_tac)
    1.20      | _ => no_tac))
    1.21  
    1.22  
    1.23 -
    1.24  (* Injection means to prove that the regularized theorem implies
    1.25     the abs/rep injected one.
    1.26