Zorn's Lemma for partial orders is now also available in ZF (see Zorn.thy). (For those who don't read the log at http://isabelle.in.tum.de/ isabelle-bin/mercurial.cgi on a regular basis.) Clemens