[isabelle] (no subject)


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

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.



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