changeset 32952 | aeb1e44fbc19 |
parent 26499 | b4db4e165758 |
child 35409 | 5c5bb83f2bae |
--- 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 =>