src/HOL/ex/Bubblesort.thy

--- a/src/HOL/ex/Bubblesort.thy	Fri Jan 19 15:50:17 2018 +0100
+++ b/src/HOL/ex/Bubblesort.thy	Sat Jan 20 16:15:05 2018 +0100
@@ -73,8 +73,7 @@
 apply(induction xs rule: bubblesort.induct)
   apply simp
  apply simp
-apply (fastforce simp: set_bubblesort split: list.split if_splits
-  intro!: sorted.Cons dest: bubble_min_min)
+apply (fastforce simp: set_bubblesort sorted_Cons split: list.split if_splits dest: bubble_min_min)
 done
 
 end