[isabelle] print_classes and records



Hello all,

I have a strange error when using the command "print_classes" after an 
extended record definition. Is this a bug ?

I'm using Isabelle2009-1.

For a minimal example:

------------------
theory aaa imports Main
begin

record foo =
  foo :: unit

print_classes (* Ok *)

record bar = foo +
  bar :: unit

print_classes (* exception Empty raised (line 477 of "library.ML") [function 
split_last] *)
------------------

Cheers

Mathieu Giorgino
theory aaa imports Main
begin

record ('a, 'v, 'r) tables =
  trees :: "('a * 'v * 'r) list set"

print_classes

Attachment: signature.asc
Description: This is a digitally signed message part.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.