Today's isatest indicates a significant drop in performance: http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Metis_Examples.png http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Metis_Examples.png http://isabelle.in.tum.de/devel/stats/mac-poly-M8/HOL-Metis_Examples.png Makarius