diff -r e4fb0daadcff -r aea892559fc5 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sat Dec 05 10:18:23 2009 +0100
+++ b/src/HOL/Predicate.thy	Sat Dec 05 20:02:21 2009 +0100
@@ -726,7 +726,7 @@
 proof (cases "f ()")
   case Empty
   thus ?thesis
-    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"]  sup_bot)
+    unfolding Seq_def by (simp add: sup_commute [of "\<bottom>"])
 next
   case Insert
   thus ?thesis