src/HOL/SEQ.thy

--- a/src/HOL/SEQ.thy	Fri Aug 28 18:11:42 2009 +0200
+++ b/src/HOL/SEQ.thy	Fri Aug 28 18:52:41 2009 +0200
@@ -582,7 +582,7 @@
       ultimately
       have "a (max no n) < a n" by auto
       with monotone[where m=n and n="max no n"]
-      show False by auto
+      show False by (auto simp:max_def split:split_if_asm)
     qed
   } note top_down = this
   { fix x n m fix a :: "nat \<Rightarrow> real"