Email Gateway (Aug 18 2022 at 14:56): Email Gateway (Aug 18 2022 at 14:56):From: Mathieu Giorgino <Mathieu.Giorgino@irit.fr>
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
print_classes_test.thy
signature.asc
Email Gateway (Aug 18 2022 at 14:56):From: Makarius <makarius@sketis.net>
Yes, this problem was introduced in the last major overhaul of the record
package, shortly before the release. It was fixed later, see
http://isabelle.in.tum.de/repos/isabelle/rev/61bb9f8af129
The included diff is a backported version of that change. You can use the
GNU patch utility to apply it to the Isabelle2009-1 sources.
Makarius
record.diff
Last updated: Apr 25 2024 at 20:15 UTC