--- a/QuotMain.thy	Thu Oct 22 15:44:16 2009 +0200
+++ b/QuotMain.thy	Thu Oct 22 15:45:05 2009 +0200
@@ -1035,7 +1035,7 @@
       instantiate_tac @{thm REP_ABS_RSP(1)} ctxt,
       instantiate_tac @{thm APPLY_RSP} ctxt,
       rtac reflex_thm,
-      Cong_Tac.cong_tac @{thm cong},
+(*      Cong_Tac.cong_tac @{thm cong},*)
       atac
     ])
 *}
@@ -1093,7 +1093,6 @@
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 (* ABS_REP_RSP *)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
@@ -1153,7 +1152,6 @@
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
@@ -1171,7 +1169,6 @@
 apply (rule allI)
 apply (rule impI)
 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *})
 apply (simp only: FUN_REL.simps)
 done