src/HOL/HOLCF/UpperPD.thy

--- a/src/HOL/HOLCF/UpperPD.thy	Wed Dec 30 21:10:19 2015 +0100
+++ b/src/HOL/HOLCF/UpperPD.thy	Wed Dec 30 21:23:38 2015 +0100
@@ -72,12 +72,10 @@
 
 subsection {* Type definition *}
 
-typedef 'a upper_pd =
+typedef 'a upper_pd  ("('(_')\<sharp>)") =
   "{S::'a pd_basis set. upper_le.ideal S}"
 by (rule upper_le.ex_ideal)
 
-type_notation (xsymbols) upper_pd ("('(_')\<sharp>)")
-
 instantiation upper_pd :: (bifinite) below
 begin