--- a/src/HOL/Tools/ATP/atp_util.ML Wed Feb 20 10:45:01 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Wed Feb 20 10:45:23 2013 +0100
@@ -287,10 +287,10 @@
| s_not t = @{const Not} $ t
fun s_conj (@{const True}, t2) = t2
| s_conj (t1, @{const True}) = t1
- | s_conj p = HOLogic.mk_conj p
+ | s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2)
fun s_disj (@{const False}, t2) = t2
| s_disj (t1, @{const False}) = t1
- | s_disj p = HOLogic.mk_disj p
+ | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2)
fun s_imp (@{const True}, t2) = t2
| s_imp (t1, @{const False}) = s_not t1
| s_imp p = HOLogic.mk_imp p