changeset 15570 | 8d8c70b41bab |
parent 15531 | 08c8dad8e399 |
child 17521 | 0f1c48de39f5 |
--- a/src/FOL/eqrule_FOL_data.ML Thu Mar 03 09:22:35 2005 +0100 +++ b/src/FOL/eqrule_FOL_data.ML Thu Mar 03 12:43:01 2005 +0100 @@ -37,14 +37,14 @@ (case Term.head_of p of Const(a,_) => (case Library.assoc(pairs,a) of - SOME(rls) => flat (map atoms ([th] RL rls)) + SOME(rls) => List.concat (map atoms ([th] RL rls)) | NONE => [th]) | _ => [th]) | _ => [th]) in atoms end; val prep_meta_eq = - (mapfilter + (List.mapPartial mk_eq o (mk_atomize tranformation_pairs) o Drule.gen_all