diff -r 672b94510e7d -r abafefa0d58b IntEx.thy
--- a/IntEx.thy	Thu Dec 03 11:33:24 2009 +0100
+++ b/IntEx.thy	Thu Dec 03 11:34:34 2009 +0100
@@ -285,8 +285,6 @@
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
 apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
 apply(simp only: nil_prs)
-apply(rule test_all_prs)
-apply(tactic {* rtac quot 1 *})
 apply(tactic {* clean_tac @{context} [quot] defs 1 *})
 done