1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Wed Feb 20 17:05:24 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Feb 20 17:12:21 2013 +0100
     1.3 @@ -287,15 +287,23 @@
     1.4    | s_not t = @{const Not} $ t
     1.5  fun s_conj (@{const True}, t2) = t2
     1.6    | s_conj (t1, @{const True}) = t1
     1.7 +  | s_conj (@{const False}, _) = @{const False}
     1.8 +  | s_conj (_, @{const False}) = @{const False}
     1.9    | s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2)
    1.10  fun s_disj (@{const False}, t2) = t2
    1.11    | s_disj (t1, @{const False}) = t1
    1.12 +  | s_disj (@{const True}, _) = @{const True}
    1.13 +  | s_disj (_, @{const True}) = @{const True}
    1.14    | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2)
    1.15  fun s_imp (@{const True}, t2) = t2
    1.16    | s_imp (t1, @{const False}) = s_not t1
    1.17 +  | s_imp (@{const False}, _) = @{const True}
    1.18 +  | s_imp (_, @{const True}) = @{const True}
    1.19    | s_imp p = HOLogic.mk_imp p
    1.20  fun s_iff (@{const True}, t2) = t2
    1.21    | s_iff (t1, @{const True}) = t1
    1.22 +  | s_iff (@{const False}, t2) = s_not t2
    1.23 +  | s_iff (t1, @{const False}) = s_not t1
    1.24    | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
    1.25  
    1.26  (* cf. "close_form" in "refute.ML" *)