diff -r 29800666e526 -r 842917225d56 src/HOL/Nominal/Examples/Standardization.thy
--- a/src/HOL/Nominal/Examples/Standardization.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -370,7 +370,7 @@
     (\<exists>t u us. x \<sharp> r \<longrightarrow> r = (Lam [x].t) \<and> rs = u # us \<and> s = t[x::=u] \<degree>\<degree> us)"
     apply (nominal_induct u \<equiv> "r \<degree>\<degree> rs" s avoiding: x r rs rule: beta.strong_induct)
     apply (simp add: App_eq_foldl_conv)
-    apply (split split_if_asm)
+    apply (split if_split_asm)
     apply simp
     apply blast
     apply simp
@@ -391,12 +391,12 @@
     apply (rule refl)
     apply (simp add: abs_fresh fresh_atm fresh_left calc_atm subst_rename)
       apply (drule App_eq_foldl_conv [THEN iffD1])
-      apply (split split_if_asm)
+      apply (split if_split_asm)
        apply simp
        apply blast
       apply (force intro!: disjI1 [THEN append_step1I] simp add: fresh_list_append)
      apply (drule App_eq_foldl_conv [THEN iffD1])
-     apply (split split_if_asm)
+     apply (split if_split_asm)
       apply simp
       apply blast
      apply (clarify, auto 0 3 intro!: exI intro: append_step1I)