--- a/QuotMain.thy	Wed Oct 28 01:49:31 2009 +0100
+++ b/QuotMain.thy	Wed Oct 28 10:17:07 2009 +0100
@@ -810,9 +810,8 @@
     val defs_pre_sym = map symmetric defs
     val defs_atom = map atomize_thm defs_pre_sym
     val defs_all = flat (map (add_lower_defs_aux ctxt) defs_atom)
-    val defs_sym = map (fn t => eq_reflection OF [t]) defs_all
   in
-    map Thm.varifyT defs_sym
+    map Thm.varifyT defs_all
   end
 *}