# HG changeset patch
# User webertj
# Date 1180767245 -7200
# Node ID d47e2daac66573dfcc356ed0206062de8b4e678f
# Parent  42004f6d908bac7e22a93dcfe16e8e142de6c19b
cosmetic

diff -r 42004f6d908b -r d47e2daac665 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Sat Jun 02 08:50:29 2007 +0200
+++ b/src/HOL/arith_data.ML	Sat Jun 02 08:54:05 2007 +0200
@@ -958,8 +958,9 @@
 
 fun raw_arith_tac ex i st =
   (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
-     decomp sg"?) to speed things up in case there are lots of irrelevant
-     terms involved; elimination of min/max can be optimized:
+     decomp sg"? -- but note that the test is applied to terms already before
+     they are split/normalized) to speed things up in case there are lots of
+     irrelevant terms involved; elimination of min/max can be optimized:
      (max m n + k <= r) = (m+k <= r & n+k <= r)
      (l <= min m n + k) = (l <= m+k & l <= n+k)
   *)