diff -r 437bd400d808 -r f9f3006a5579 src/HOL/NanoJava/Example.thy
--- a/src/HOL/NanoJava/Example.thy	Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/NanoJava/Example.thy	Wed Aug 10 09:33:54 2016 +0200
@@ -184,7 +184,7 @@
 apply   rule
 apply   (rule hoare_ehoare.Asm) (* 20 *)
 apply   (rule_tac a = "((case n of 0 \<Rightarrow> 0 | Suc m \<Rightarrow> m),m+1)" in UN_I, rule+)
-apply  (clarsimp split add: nat.split_asm dest!: Nat_atleast_mono)
+apply  (clarsimp split: nat.split_asm dest!: Nat_atleast_mono)
 apply rule
 apply (rule hoare_ehoare.Call) (* 21 *)
 apply   (rule hoare_ehoare.LAcc)