src/ZF/arith_data.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15965 f422f8283491
     1.1 --- a/src/ZF/arith_data.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/ZF/arith_data.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4  fun prove_conv name tacs sg hyps xs (t,u) =
     1.5    if t aconv u then NONE
     1.6    else
     1.7 -  let val hyps' = filter (not o is_eq_thm) hyps
     1.8 +  let val hyps' = List.filter (not o is_eq_thm) hyps
     1.9        val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
    1.10          FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
    1.11    in SOME (hyps' MRS Tactic.prove sg xs [] goal (K (EVERY tacs)))