--- a/QuotMain.thy	Wed Oct 28 15:25:36 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 16:05:59 2009 +0100
@@ -397,10 +397,10 @@
 ML {*
 fun atomize_thm thm =
 let
-  val thm' = forall_intr_vars thm
+  val thm' = Thm.freezeT (forall_intr_vars thm)
   val thm'' = ObjectLogic.atomize (cprop_of thm')
 in
-  Thm.freezeT @{thm Pure.equal_elim_rule1} OF [thm'', thm']
+  @{thm Pure.equal_elim_rule1} OF [thm'', thm']
 end
 *}