[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

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] *)


Mathieu Giorgino
theory aaa imports Main

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


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

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