--- 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]]