Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 23 Sep 1993 17:05:44 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA25697;
          Thu, 23 Sep 93 08:59:04 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from mahogany.cs.ucdavis.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA25693; Thu, 23 Sep 93 08:58:58 -0700
Received: from localhost.cs.ucdavis.edu 
          by mahogany.cs.ucdavis.edu (5.65/UCD.CS.2.4) id AA21173;
          Thu, 23 Sep 1993 08:59:01 -0700
Message-Id: <9309231559.AA21173@mahogany.cs.ucdavis.edu>
To: info-hol@cs.uidaho.edu
Cc: benson@cs.ucdavis.edu
Subject: loading more_lists fails.
Date: Thu, 23 Sep 93 08:59:00 -0700
From: shaw@cs.ucdavis.edu
X-Mts: smtp


My current version of more_lists.ml in HOL88 v. 2.01 contains:

% --------------------------------------------------------------------- %
% Load compiled code if possible                                        %
% --------------------------------------------------------------------- %

if (draft_mode() or (current_theory() = `more_lists`)) then
   let path st = library_pathname() ^ `/more_lists/` ^ st in
-->    (load_auxiliary();
        load(path `list_imec_tactics`, get_flag_value `print_lib`));;

but load_auxiliary in not previously defined anywhere in this file. Whether I
load_library `more_lists` directly, or load auxiliary and more_arithmetic myself
first, the loading of more_lists bombs at the load_auxiliary with the usual
"unbound or non-assignable var...". Moreover, the very top of this file does a
load_library `auxiliary` anyway.

For now, I'll just define a nop load_auxiliary, but do I have an incomplete or
otherwise incorrect version of more_lists.ml for 88 v. 2.01?

Thanx!

Rob