# HG changeset patch
# User huffman
# Date 1313731939 25200
# Node ID 453803d28c4b003d4b1080ef1b3d1c3dda6d00c8
# Parent  dbd9965745fdb4b5858d039b447c69aab74462c7# Parent  dd203341fd2bb8e5227dc192a4966e51e1c1f34c
merged

diff -r dbd9965745fd -r 453803d28c4b src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Aug 18 22:31:52 2011 -0700
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Aug 18 22:32:19 2011 -0700
@@ -168,7 +168,7 @@
     val eq_eqvs = eq_imp_rel_get ctxt
   in
     simp_tac simpset THEN'
-    REPEAT_ALL_NEW (CHANGED o FIRST'
+    TRY o REPEAT_ALL_NEW (CHANGED o FIRST'
       [resolve_tac @{thms ball_reg_right bex_reg_left bex1_bexeq_reg},
        resolve_tac (Inductive.get_monos ctxt),
        resolve_tac @{thms ball_all_comm bex_ex_comm},
@@ -396,12 +396,12 @@
     Cong_Tac.cong_tac @{thm cong} THEN'
                  RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
 
+    (* resolving with R x y assumptions *)
+    atac,
+
     (* (op =) (%x...) (%y...) ----> (op =) (...) (...) *)
     rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
 
-    (* resolving with R x y assumptions *)
-    atac,
-
     (* reflexivity of the basic relations *)
     (* R ... ... *)
     resolve_tac rel_refl]