# HG changeset patch
# User blanchet
# Date 1361353523 -3600
# Node ID 1c6031e5d284d5e9e8e1b9a1eddb8d85a86d9999
# Parent  1ff19dfd3111af43282d04e23593da3388293310
optimize Isar output some more

diff -r 1ff19dfd3111 -r 1c6031e5d284 src/HOL/Tools/ATP/atp_util.ML
--- 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