[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"
   where
  "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.

Best,
Randy


--
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.