1.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Aug 18 23:43:22 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Aug 19 10:23:16 2011 +0900
     1.3 @@ -168,7 +168,7 @@
     1.4      val eq_eqvs = eq_imp_rel_get ctxt
     1.5    in
     1.6      simp_tac simpset THEN'
     1.7 -    REPEAT_ALL_NEW (CHANGED o FIRST'
     1.8 +    TRY o REPEAT_ALL_NEW (CHANGED o FIRST'
     1.9        [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
    1.10         resolve_tac (Inductive.get_monos ctxt),
    1.11         resolve_tac @{thms ball_all_comm bex_ex_comm},
    1.12 @@ -396,12 +396,12 @@
    1.13      Cong_Tac.cong_tac @{thm cong} THEN'
    1.14                   RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
    1.15  
    1.16 +    (* resolving with R x y assumptions *)
    1.17 +    atac,
    1.18 +
    1.19      (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
    1.20      rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
    1.21  
    1.22 -    (* resolving with R x y assumptions *)
    1.23 -    atac,
    1.24 -
    1.25      (* reflexivity of the basic relations *)
    1.26      (* R ... ... *)
    1.27      resolve_tac rel_refl]