[isabelle-dev] interpretation command: "show ?thesis" causes type error

[Brian Huffman]

When proving a lemma, the term abbreviation ?thesis typically has type
"bool", and saying "show ?thesis" usually works.

But with "interpretation", it doesn't work. Here is a toy example that
shows what I mean:


locale foo = fixes x :: "'a::type" assumes x: "x = x"

term "foo" (* it has type 'a => bool, as expected. *)

interpretation myfoo: foo True
proof -
  term ?thesis  (* "foo True" :: prop *)
  show ?thesis

*** Type unification failed: Clash of types "prop" and "bool"
***
*** Type error in application: incompatible operand type
***
*** Operator:  Trueprop :: bool => prop
*** Operand:   PROP ?thesis :: prop
***
*** At command "show"

I am using revision 1410c84013b9, but the same error occurs with the
last few release versions as well.

- Brian