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; Thu, 17 Jun 1993 17:38:14 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15413;
          Thu, 17 Jun 93 07:26:42 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA15408;
          Thu, 17 Jun 93 07:26:32 -0700
Received: from woodcock.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Thu, 17 Jun 1993 15:26:35 +0100
To: info-hol@ted.cs.uidaho.edu
Subject: HOL88 ML function type_in
Date: Thu, 17 Jun 93 15:26:30 +0100
From: Wai Wong <Wai.Wong@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:171220:930617142642"@cl.cam.ac.uk>


It has been found that the ML function type_in in HOL88 has some
undesired strange behaviour. Since it is not used in the system
itself, it is proposed to be deleted from the next version (ver.
2.02). If anyone  has any objection please let me know. 

Wai