Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Message-Id: <199509010114.AA060958050@puma.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: HOL90 error on 'export_theory'
Date: Thu, 31 Aug 1995 19:14:09 -0600
From: Kelly Hall <hall@cs.byu.edu>

Hello HOL90 gurus worldwide!

I got HOL90.7 to build successfully (?) on our HP 735 with SML/NJ
0.93.  While trying to build the contrib stuff, I've been getting
errors (HOL_ERR exceptions) when 'export_theory()' is called.

Is there a way for me to get a more enlightening error message than
the uncaught exception (that goes scrolling merrily off the screen)?

Secondly, does anyone have an idea what's causing this exception?
I'll include a transcript of the problem, but it isn't very
interesting reading.

Running the contrib/bmark code yields:
----------------------------------------
.. (much normal-looking stuff deleted)
..
val s_tm = . |- s (SUC x + d) = FN (i (SUC x),g (i (SUC x),s (SUC x))) : thm
val NEXT_THM =
  |- !FN f g done i s.
       (!x. (done x = f (s x)) /\ (s (x + 1) = g (i x,s x))) /\
       (!a b. FN (a,b) = ((f b) => b | (FN (a,g (a,b))))) ==>
       (!d x.
         NEXT (x,x + d) done /\ STABLE (x,x + d) i ==>
         (s (x + d) = FN (i x,g (i x,s x)))) : thm

Theory "NEXT" closed.
val it = () : unit

uncaught exception HOL_ERR
----------------------------------------

Frankly, I'm pleased as punch that I could even get HOL90 loaded this
far.  I only noticed this problem when I was trying to get a benchmark
number for HOL90 + HPs.

Thanks in advance for any help,
Kelly