--- a/src/HOL/ex/Bubblesort.thy	Sun May 06 23:59:14 2018 +0100
+++ b/src/HOL/ex/Bubblesort.thy	Tue May 08 10:14:36 2018 +0200
@@ -73,7 +73,7 @@
 apply(induction xs rule: bubblesort.induct)
   apply simp
  apply simp
-apply (fastforce simp: set_bubblesort sorted_Cons split: list.split if_splits dest: bubble_min_min)
+apply (fastforce simp: set_bubblesort split: list.split if_splits dest: bubble_min_min)
 done
 
 end