--- a/src/HOL/Matrix_LP/Matrix.thy Tue Feb 23 15:37:18 2016 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy Tue Feb 23 16:25:08 2016 +0100
@@ -1653,8 +1653,8 @@
lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
apply (simp add: one_matrix_def)
apply (simplesubst RepAbs_matrix)
-apply (rule exI[of _ n], simp add: split_if)+
-by (simp add: split_if)
+apply (rule exI[of _ n], simp add: if_split)+
+by (simp add: if_split)
lemma nrows_one_matrix[simp]: "nrows ((one_matrix n) :: ('a::zero_neq_one)matrix) = n" (is "?r = _")
proof -