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; Tue, 6 Jun 1995 19:32:51 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA006050921;
          Tue, 6 Jun 1995 11:48:41 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from cheetah.cs.byu.edu by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA006010920;
          Tue, 6 Jun 1995 11:48:41 -0600
From: Clark Barrett <barrett@lal.cs.byu.edu>
Received: by cheetah.cs.byu.edu (1.37.109.15/CS-Client) id AA276750909;
          Tue, 6 Jun 1995 11:48:29 -0600
Message-Id: <199506061748.AA276750909@cheetah.cs.byu.edu>
Subject: ML/HOL strings
To: info-hol@leopard.cs.byu.edu
Date: Tue, 06 Jun 1995 11:48:28 MDT
X-Mailer: Elm [revision: 109.14]


I need an ML function which converts an ML string `foo` to a hol term
which is the same string "`foo`:string".  Has anyone found a simple
(or even not so simple) way of doing this?

I was thinking that if the HOL parser could be invoked directly, that
would be a solution.  Does anyone know how to do this?

Thanks,
Clark Barrett
barrett@lal.cs.byu.edu