[Gcl-devel] HOL88 and GCL

[Camm Maguire]

Greetings, and please excuse my intrusion on your mailbox.  Robert
Boyer suggested I write to you.  I am currently the lead GCL
developer, and we are preparing a new release.  One of the goals of
GCL development has been to preserve whatever capabilities it or its
ancestors had as we move toward ANSI compliance.   To this end I've
noticed that an older version of HOL, HOL88 used to build on akcl and
early GCL.  I know this old version is likely of no interest to anyone
any longer, but I would nevertheless like to satisfy myself that GCL
will still build it.  

The build goes on for quite a while before giving the following ML
error.  Would you happen to be able to shed any light or offer any
suggestions?

Take care, 

=============================================================================
address@hidden:/fix/t1/camm/debian/gcl/hol88/hol$ make hol
cd /fix/t1/camm/debian/gcl/hol88/hol/theories; rm -f ind.th;\
/fix/t1/camm/debian/gcl/hol88/hol/hol-lcf < 
/fix/t1/camm/debian/gcl/hol88/hol/theories/mk_ind.ml;\
cd /fix/t1/camm/debian/gcl/hol88/hol

HOL-LCF version 2.02 (SUN4/AKCL) created 22/10/5

############################() : void

##Theory bool loaded
() : void

##() : void

##
() : void

() : void

() : void

() : void

() : void

() : void

() : void

() : void

........() : void

...................................................................................................................................()
 : void


File /fix/t1/camm/debian/gcl/hol88/hol/ml/hol-in-out loaded
() : void

##Badly typed application of:  "/\"
   which has type:           ":NIL"
to the argument term:        "ONE_ONE f"
   which has type:           ":?"

evaluation failed     mk_comb in quotation
=======> theory ind built
=============================================================================

-- 
Camm Maguire                                            address@hidden
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah