diff -r 18500bd1f47b -r 655f583840d0 src/HOL/HOLCF/LowerPD.thy --- a/src/HOL/HOLCF/LowerPD.thy Sat Jan 08 10:02:43 2011 -0800 +++ b/src/HOL/HOLCF/LowerPD.thy Sat Jan 08 11:18:09 2011 -0800 @@ -136,7 +136,7 @@ "xs \\ ys == lower_plus\xs\ys" syntax - "_lower_pd" :: "args \ 'a lower_pd" ("{_}\") + "_lower_pd" :: "args \ logic" ("{_}\") translations "{x,xs}\" == "{x}\ \\ {xs}\"