changeset 15570 | 8d8c70b41bab |
parent 15531 | 08c8dad8e399 |
child 17002 | fb9261990ffe |
--- a/src/ZF/simpdata.ML Thu Mar 03 09:22:35 2005 +0100 +++ b/src/ZF/simpdata.ML Thu Mar 03 12:43:01 2005 +0100 @@ -16,7 +16,7 @@ case head_of t of Const(a,_) => (case assoc(pairs,a) of - SOME rls => flat (map (atomize (conn_pairs, mem_pairs)) + SOME rls => List.concat (map (atomize (conn_pairs, mem_pairs)) ([th] RL rls)) | NONE => [th]) | _ => [th]