src/ZF/simpdata.ML

--- a/src/ZF/simpdata.ML	Thu Apr 29 22:08:57 2010 +0200
+++ b/src/ZF/simpdata.ML	Thu Apr 29 22:56:32 2010 +0200
@@ -44,7 +44,7 @@
 val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
 
 change_simpset (fn ss =>
-  ss setmksimps (map mk_eq o ZF_atomize o gen_all)
+  ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
   addcongs [@{thm if_weak_cong}]);
 
 local