diff -r 4d9518c3d031 -r b66d2ca1f907 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -119,12 +119,10 @@
 
 subsection {* Type definition *}
 
-typedef 'a convex_pd =
+typedef 'a convex_pd  ("('(_')\<natural>)") =
   "{S::'a pd_basis set. convex_le.ideal S}"
 by (rule convex_le.ex_ideal)
 
-type_notation (xsymbols) convex_pd ("('(_')\<natural>)")
-
 instantiation convex_pd :: (bifinite) below
 begin