[isabelle-dev] Type error in metis call with Toplevel.debug
krauss at in.tum.de
Fri Jun 12 13:46:54 CEST 2009
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