[isabelle] use_thy "Pure";



In an attempt to build the raw Isabelle process,
I am trying to get my ML system to make sense of this file:
src/Pure/ROOT.ML
It goes fine till the point when its given

use_thy "Pure";

upon when it complains with the following.

------------
Loading theory "Pure
*** Uninitialized theory data "Isar/attributes"
------------

I have made some changes to the source inorder to suit the dialect of ML that I am using (alice). I have been trying to investigate if this error is because of

(1)-any of the changes that i have made
(2)-of the implementation features of alice

I can say that (2) is not the case, as i have tried the same experiment (with the same source) in the SML-NJ system and i get the same error.

I am wondering if any of you have ever done something like this before and if you can help.

I will be very grateful for any info on the sequence of function calls involved in "use_thy" and the dependecies.

Thanks in advance for your help,

Priya






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