--- a/QuotMain.thy	Thu Oct 22 16:10:06 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 16:24:02 2009 +0200
@@ -1024,6 +1024,15 @@
 *}
 
 ML {*
+fun res_forall_rsp_tac ctxt =
+  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+  THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+  THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+  (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
+*}
+
+
+ML {*
 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm =
   (FIRST' [
     rtac @{thm FUN_QUOTIENT},
@@ -1031,6 +1040,7 @@
     rtac @{thm IDENTITY_QUOTIENT},
     rtac @{thm ext},
     rtac trans_thm,
+    res_forall_rsp_tac ctxt,
       instantiate_tac @{thm REP_ABS_RSP(1)} ctxt,
       instantiate_tac @{thm APPLY_RSP} ctxt,
       rtac reflex_thm,
@@ -1056,12 +1066,7 @@
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (simp only: FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (simp only: FUN_REL.simps)
+apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RES_TAC *)
@@ -1092,12 +1097,7 @@
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 (* ABS_REP_RSP *)
-apply (simp only: FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (simp only: FUN_REL.simps)
+apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 (* LAMBDA_RSP *)
 apply (simp only: FUN_REL.simps)
@@ -1150,12 +1150,7 @@
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
-apply (simp only: FUN_REL.simps)
-apply (rule allI)
-apply (rule allI)
-apply (rule impI)
-apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (simp only: FUN_REL.simps)
+apply (tactic {* r_mk_comb_tac_fset @{context} 1 *})
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 apply (rule allI)