[isabelle-dev] Type error in metis call with Toplevel.debug

[Alexander Krauss]

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