[isabelle] uncaught exception from Isabelle 2009-2
In Isabelle 2009-2:
theory bugSatoHS imports Nominal begin
nominal_datatype trm1 = tpar par
and trm2 = atrm
nominal_primrec p1sub1 :: "trm1 => trm1 => par => trm1"
"p1sub1 (tpar p) t q = t"
*** exception Subscript raised (line 97 of "./basis/List.sml")
*** At command "nominal_primrec".
The problem seems to be that the "mutual" part of the primrec
definition for trm2 is missing.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and