[isabelle] uncaught exception from Isabelle 2009-2

In Isabelle 2009-2:

 theory bugSatoHS imports Nominal begin
 atom_decl par
 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 MHonArc.