diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -46,7 +46,7 @@
 apply (simp add: int_of_real_sub real_int_of_real)
 done
 
-lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real_of_int a = x"
+lemma real_is_int_rep: "real_is_int x \<Longrightarrow> \<exists>!(a::int). real_of_int a = x"
 by (auto simp add: real_is_int_def)
 
 lemma int_of_real_mult: