--- a/src/FOLP/IFOLP.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/FOLP/IFOLP.ML Thu Mar 03 12:43:01 2005 +0100
@@ -78,7 +78,7 @@
and concl = discard_proof (Logic.strip_assums_concl prem)
in
if exists (fn hyp => hyp aconv concl) hyps
- then case distinct (filter (fn hyp=> could_unify(hyp,concl)) hyps) of
+ then case distinct (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
[_] => assume_tac i
| _ => no_tac
else no_tac
@@ -310,7 +310,7 @@
(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
val pred_congs =
- flat (map (fn c =>
+ List.concat (map (fn c =>
map (fn th => read_instantiate [("P",c)] th)
[pred1_cong,pred2_cong,pred3_cong])
(explode"PQRS"));