diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -1429,7 +1429,7 @@
 
 theorem UP_universal_property:
   assumes S: "s \<in> carrier S"
-  shows "EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
+  shows "\<exists>!Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
     Phi (monom P \<one> 1) = s &
     (ALL r : carrier R. Phi (monom P r 0) = h r)"
   using S eval_monom1