[isabelle-dev] superfluous [?]

[Makarius]

On Wed, 10 Oct 2012, Ondřej Kunčar wrote:

> This problem refers to 3fc6b3289c31.
>
> If I type in this simple formalization
>
> lemma c: "x = x"
> by metis
>
> thm c
>
> the following theorem is printed "?x = ?x  [?]". What is that suspicious 
> question mark? It seems to be produced by any metis call. And it is 
> reproducible almost always.

This is the normal result of printing Thm.status_of in the traditional 
way.  It is now getting in the way, because terminal proofs ('by') are 
always parallel in Isabelle/jEdit.

I am about to rework this critical kernal status information, but it 
requires some more thinking.  Last time I changed something there, it was 
immediately reported as "problem" that fewer [!] were printed as before.


 	Makarius