--- a/QuotMain.thy	Wed Oct 28 15:25:11 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 15:25:36 2009 +0100
@@ -400,7 +400,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
 *}