--- a/QuotMain.thy	Fri Dec 04 09:01:13 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 09:08:51 2009 +0100
@@ -1287,7 +1287,7 @@
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2,
+               rtac thm THEN' all_inj_repabs_tac' lthy quot rel_refl trans2,
                clean_tac lthy quot]]
     end) lthy
 *}