diff -r 83392f9d303f -r aeb1e44fbc19 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Thu Oct 15 23:10:35 2009 +0200
+++ b/src/ZF/simpdata.ML	Thu Oct 15 23:28:10 2009 +0200
@@ -16,9 +16,8 @@
           case head_of t of
               Const(a,_) =>
                 (case AList.lookup (op =) pairs a of
-                     SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs))
-                                       ([th] RL rls))
-                   | NONE     => [th])
+                     SOME rls => maps (atomize (conn_pairs, mem_pairs)) ([th] RL rls)
+                   | NONE => [th])
             | _ => [th]
   in case concl_of th of
          Const("Trueprop",_) $ P =>