src/ZF/arith_data.ML

--- a/src/ZF/arith_data.ML	Thu Mar 03 09:22:35 2005 +0100
+++ b/src/ZF/arith_data.ML	Thu Mar 03 12:43:01 2005 +0100
@@ -71,7 +71,7 @@
 fun prove_conv name tacs sg hyps xs (t,u) =
   if t aconv u then NONE
   else
-  let val hyps' = filter (not o is_eq_thm) hyps
+  let val hyps' = List.filter (not o is_eq_thm) hyps
       val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
         FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
   in SOME (hyps' MRS Tactic.prove sg xs [] goal (K (EVERY tacs)))