diff -r 437bd400d808 -r f9f3006a5579 src/Doc/Tutorial/Inductive/AB.thy
--- a/src/Doc/Tutorial/Inductive/AB.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/Doc/Tutorial/Inductive/AB.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -264,7 +264,7 @@
 *}
 
   apply(force simp add: min_less_iff_disj)
- apply(force split add: nat_diff_split)
+ apply(force split: nat_diff_split)
 
 txt{*
 The case @{prop"w = b#v"} is proved analogously:
@@ -278,7 +278,7 @@
 apply(rule_tac n1=i and t=v in subst[OF append_take_drop_id])
 apply(rule S_A_B.intros)
  apply(force simp add: min_less_iff_disj)
-by(force simp add: min_less_iff_disj split add: nat_diff_split)
+by(force simp add: min_less_iff_disj split: nat_diff_split)
 
 text{*
 We conclude this section with a comparison of our proof with