[isabelle] (no subject)



Hello,

I am compiling Isabelle using a flavour of ML called alice.
While loading the ROOT.ML file (src/Pure/ROOT.ML) at the alice ML shell-level,
it interprets most of it fine, and gets stuck at the point when the following is invoked:

=========
use_thy "Pure"; structure Pure = struct val thy = theory "Pure" end;

use_thy "CPure"; structure CPure = struct val thy = theory "CPure" end;
=========

Here are the details:

On giving the shell
=============
use_thy "Pure";
=============

it gives

=============
Uncaught exception
   ERROR
=============

with this message:
=============
Loading theory "Pure"
*** Uninitialized theory data "Isar/attributes"
*** At command "lemma" (line 18 of "~/Priya/Work/IsabelleTest/Isabelle2005/src/Pure/Pure.thy")
=============

I will be grateful for any info on the possible reasons for a message like this and how it can be fixed.

Thanks,

Priya







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.