[isabelle-dev] [Fwd: Small problem in print translation for records]

[Florian Haftmann]

Anyone aware of the following problem?  Seems to be a corrupted syntax
translation or such.

	Florian

-------- Original Message --------
Subject: Small problem in print translation for records
Date: Sun, 23 Sep 2007 14:08:08 +0900 (JST)
From: Yasuhiko Minamide <minamide at score.cs.tsukuba.ac.jp>
To: florian.haftmann at in.tum.de
CC: minamide at cs.tsukuba.ac.jp

Dear Florian Haftmann,

I would like to report you a small problem I encoutered during my
development. (Since it is a small problem, I hesitate to post it
to the isabelle mailing list.)

I encounter the following problem in print translation
when a polymorphic record over multiple classes are used.

-----------------------------------------------
record 'a r =
  f :: 'a

term "x::'a::{finite,order} r"
-----------------------------------------------

The error message below is raised when 'Show types' and 'Show sorts' are
on in ProofGeneral setting.

Error Message
*** exception TERM raised: sort_of_term: bad encoding of classes
*** Error in print translation for "r_ext_type"
*** At command "term".

No error message is raised when 'Show sorts' is off.
The problem can be avoided by setting 'Show sorts' off, but it was rather
confusing to me.

Yasuhiko Minamide
-------------- next part --------------
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20070925/7696073f/attachment-0002.vcf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20070925/7696073f/attachment.sig>