src/ZF/arith_data.ML
changeset 33317 b4534348b8fd
parent 32155 e2bf2f73b0c8
child 35408 b48ab741683b
     1.1 --- a/src/ZF/arith_data.ML	Thu Oct 29 16:59:12 2009 +0100
     1.2 +++ b/src/ZF/arith_data.ML	Thu Oct 29 17:58:26 2009 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  fun prove_conv name tacs ctxt prems (t,u) =
     1.5    if t aconv u then NONE
     1.6    else
     1.7 -  let val prems' = List.filter (not o is_eq_thm) prems
     1.8 +  let val prems' = filter_out is_eq_thm prems
     1.9        val goal = Logic.list_implies (map (#prop o Thm.rep_thm) prems',
    1.10          FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
    1.11    in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))