--- a/QuotMain.thy	Sun Nov 29 03:59:18 2009 +0100
+++ b/QuotMain.thy	Sun Nov 29 08:48:06 2009 +0100
@@ -1094,7 +1094,7 @@
             TRY o simp_tac simp_ctxt,
             TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
             TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
-            rtac refl]
+            TRY o rtac refl]
   end
 *}