Dear isabelle-dev, Andy Schropp found the following weird behaviour, which seems to be both in Isabelle2009 and the current developer version (reproduced in b63d253ed9e2).
Steps to reproduce: - Starting from Pure or HOL-Plain, load List.thy in PG - Enable Toplevel.debug - The metis call in lemma "sorted_distinct_set_unique", fails with *** exception TERM raised: fastype_of: expected function type When Toplevel.debug is switched off then it works, so my guess is that it is related to the pretty printing of some of the debug messages, but I am not sure. Any ideas? Anybody inclined to debug this further? Alex
