diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -349,7 +349,7 @@
     by (rule while_option_rule[OF _ assms[unfolded rtrancl_while_def]])
   { assume "ws = []"
     hence ?thesis using I
-      by (auto simp del:Image_Collect_split dest: Image_closed_trancl)
+      by (auto simp del:Image_Collect_case_prod dest: Image_closed_trancl)
   } moreover
   { assume "ws \<noteq> []"
     hence ?thesis using I while_option_stop[OF assms[unfolded rtrancl_while_def]]