time + date_part oddness?

I am writing an article of PostgreSQL 7.1 and have some questions.

I can get the millisecond part of a timestamp data using date_part.

test=# SELECT date_part('millisecond','2001/1/15 12:04:05.1234'::TIMESTAMP);
date_part
-----------
123.4
(1 row)

However if I apply the function to a time data, I get a strange result.

test=# SELECT date_part('millisecond','12:04:05.1234'::time);
date_part
------------------
5123.39999999676
(1 row)

Any thought?

(This is current)
--
Tatsuo Ishii