Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 18 Jun 1993 08:11:39 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17527;
          Fri, 18 Jun 93 00:00:47 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA17522;
          Fri, 18 Jun 93 00:00:37 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA21146;
          Fri, 18 Jun 93 00:00:57 -0700
Message-Id: <9306180700.AA21146@maui.cs.ucla.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Bug in parsing object-level lists
Date: Fri, 18 Jun 93 00:00:54 PDT
From: chou@cs.ucla.edu

HOL88 seems to be unable to parse certain object-level lists:

#"[1;2;3]";;
"[1;2;3]" : term

#"[[1]]";;
"[[1]]" : term

#"[[1];[2]]";;
`;` in the wrong place
skipping: ] ; [ 2 ] ] " ;; parse failed     

#"[(CONS 1 NIL);[2]]";;
"[[1];[2]]" : term

#"[[1];(CONS 2 NIL)]";;
`;` in the wrong place
skipping: ] ; ( CONS 2 NIL ) ] " ;; parse failed     

I'd like to know if there's a patch that does not need a re-compilation
of the whole system.


- Ching Tsun