Quotient Package: Regularization: do not fail if no progress is made, leave the subgoal to the user. Injection: try assumptions before extensionality to avoid looping.

--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Thu Aug 18 23:43:22 2011 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Fri Aug 19 10:23:16 2011 +0900
@@ -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]