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

Alexander Krauss krauss at in.tum.de
Fri Jun 12 13:46:54 CEST 2009

Dear isabelle-dev,

Andy Schropp found the following weird behaviour, which seems to be both 
in Isabelle2009 and the current developer version (reproduced in 

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?


More information about the isabelle-dev mailing list