Changesets f523923d8182 and 3bc39cfe27fe should have resolved the issue.
Lukas
On 09/02/2011 11:40 AM, Lukas Bulwahn wrote:
The reason that this issue has just recently become apparent, is due
to changes 322d1657c40c ff. by Andreas Lochbihler. He assisted in
replacing (Stefan Berghofer's) SML
Changesets f523923d8182 and 3bc39cfe27fe should have resolved the issue.
Thanks a lot, I have overlooked the other occurence.
I suggest to move the symbolic name identifier to code_target and
reference it uniformly from all ocurrences.
Florian
--
Home:
http://www.in.tum.de/~haftmann
The reason that this issue has just recently become apparent, is due to
changes 322d1657c40c ff. by Andreas Lochbihler. He assisted in replacing
(Stefan Berghofer's) SML code generator invocations by generic code
generator invocations to enable the long-term removal of the SML code
generator.
For quite some time isatest produces the following error with SML/NJ:
Loading theory Executable_Set
*** Error in
/mnt/home/isatest/isadist/Isabelle_29-Aug-2011/src/HOL/Library/Executable_Set.thy
*** instream:2.3-2.20 Error: unbound variable or constructor: add_type_cmd in
path
