--- a/src/HOL/UNITY/Simple/Channel.thy	Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/UNITY/Simple/Channel.thy	Tue Feb 23 16:25:08 2016 +0100
@@ -29,7 +29,7 @@
 (*None represents "infinity" while Some represents proper integers*)
 lemma minSet_eq_SomeD: "minSet A = Some x ==> x \<in> A"
 apply (unfold minSet_def)
-apply (simp split: split_if_asm)
+apply (simp split: if_split_asm)
 apply (fast intro: LeastI)
 done