src/HOL/Predicate.thy

      | Insert x P \<Rightarrow> Insert x (P \<squnion> Seq g)
      | Join P xq \<Rightarrow> adjunct (Seq g) (Join P xq))"
 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
     unfolding Seq_def by (simp add: sup_assoc)
 next