Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 30 Dec 1993 23:17:43 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA01820;
          Thu, 30 Dec 1993 16:08:14 -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 AA01816;
          Thu, 30 Dec 1993 16:08:13 -0700
Received: from inet-gw-2.pa.dec.com by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA01795;
          Thu, 30 Dec 1993 15:05:51 -0800
Received: by inet-gw-2.pa.dec.com; id AA03647; Wed, 29 Dec 93 16:59:43 -0800
Received: by evsrv3.afl.hlo.dec.com (5.57/ULTRIX-fma-041391); id AA00553;
          Wed, 29 Dec 93 19:59:41 -0500
Date: Wed, 29 Dec 93 19:59:41 -0500
From: leonard@evsrv3.afl.hlo.dec.com (Tim Leonard)
Message-Id: <9312300059.AA00553@evsrv3.afl.hlo.dec.com>
To: info-hol@cs.uidaho.edu
Subject: A problem in hol88 parsing "CONS ~O ops"

I found a little problem in the hol88 parser today.  It shows up when parsing
a term with "CONS" applied to a subterm starting with "~".  Here are the
symptoms:

#"CONS ~O ops";;
Indeterminate types:  "O:? -> bool"

evaluation failed     types indeterminate in quotation

#"CONS (~O) ops";;
"CONS~Oops" : term
Run time: 0.0s

#