src/HOL/HOLCF/LowerPD.thy

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