--- a/src/HOL/simpdata.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/simpdata.ML Thu Mar 03 12:43:01 2005 +0100
@@ -253,14 +253,14 @@
(case head_of p of
Const(a,_) =>
(case 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;
fun mksimps pairs =
- (mapfilter (try mk_eq) o mk_atomize pairs o gen_all);
+ (List.mapPartial (try mk_eq) o mk_atomize pairs o gen_all);
fun unsafe_solver_tac prems =
FIRST'[resolve_tac(reflexive_thm::TrueI::refl::prems), atac, etac FalseE];