Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 11 Jan 1994 11:47:35 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA12821; Tue, 11 Jan 1994 04:41:30 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA12817; Tue, 11 Jan 1994 04:41:28 -0700 Received: from [129.215.160.108] by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA12279; Tue, 11 Jan 1994 03:39:24 -0800 Date: Tue, 11 Jan 1994 03:39:24 -0800 Received: from applecross.dcs.ed.ac.uk by dcs.ed.ac.uk id aa08776; 11 Jan 94 11:35 GMT X-Sender: kevin@campay Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" To: info-hol@cs.uidaho.edu From: Kevin Mitchell Subject: A problem building Hol90.6 Message-Id: <9401111135.aa08776@dcs.ed.ac.uk> I've just finished building version 6 of hol90 and am having some problems with the libraries. After a bit of investigation, I narrowed the problem down to the following example. I'd appreciate any suggestions for where to go from here. Thanks, Kevin. - new_theory "boo"; Declaring theory "boo". Theory "HOL" already consistent with disk, hence not exported. val it = () : unit - new_parent "string" handle e => Raise e; Exception raised at Theory.new_parent.install_new_parent.install_hol_sig.add_ter m_const: Term constant clash: RES_ABSTRACT appears in both restr_binder and restr_binder uncaught exception HOL_ERR - parents "-"; val it = ["HOL"] : string list (* However, if I now try the same command again it appears to work! *) - new_parent "string" handle e => Raise e; val it = () : unit - parents "-"; val it = ["string","HOL"] : string list