--- a/QuotMain.thy	Wed Oct 28 12:22:06 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 14:59:24 2009 +0100
@@ -355,7 +355,7 @@
   val thm' = forall_intr_vars thm
   val thm'' = ObjectLogic.atomize (cprop_of thm')
 in
-  Thm.freezeT (Simplifier.rewrite_rule [thm''] thm')
+  Thm.freezeT @{thm Pure.equal_elim_rule1} OF [thm'', thm']
 end
 *}