Return-Path: 
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from nsf.ac.uk by swan.cl.cam.ac.uk via JANET 
          with NIFTP to fgate (PP) id <18999-0@swan.cl.cam.ac.uk>;
          Sat, 23 Feb 1991 18:08:06 +0000
Received: from vax.nsfnet-relay.ac.uk by sun2.nsfnet-relay.ac.uk 
          with SMTP inbound id <24109-225@sun2.nsfnet-relay.ac.uk>;
          Sat, 23 Feb 1991 02:53:01 +0000
Received: from iris.ucdavis.edu by vax.NSFnet-Relay.AC.UK via NSFnet with SMTP 
          id aa26931; 23 Feb 91 1:41 GMT
Received: by iris.eecs.ucdavis.edu (5.57/UCD.EECS.4.0) id AA09386;
          Wed, 20 Feb 91 20:58:32 -0800
Received: from munnari.OZ.AU by clover.eecs.ucdavis.edu (5.59/UCD.EECS.1.11) 
          id AA07432; Wed, 20 Feb 91 21:00:02 PST
Received: from itd.dsto.oz (via augean) by munnari.oz.au 
          with SunIII (5.64+1.3.1+0.50) id AA12369;
          Thu, 21 Feb 1991 15:58:16 +1100 (from cant@itd.dsto.oz.au)
Received: from itd0.dsto.oz (itd0.ARPA) by fang.dsto.oz (1.2/4.7) id AA23960;
          Thu, 21 Feb 91 15:30:17 pdt
Received: from tcs12.dsto.oz by itd0.dsto.oz (4.1/SMI-3.2) id AA15735;
          Thu, 21 Feb 91 15:25:21 CST
Date: Thu, 21 Feb 91 15:25:21 CST
From: cant@au.oz.dsto.itd (Tony Cant)
Message-Id: <9102210455.AA15735@itd0.dsto.oz>
To: info-hol@edu.ucdavis.clover
Subject: String to term conversion
Sender: cant <cant%au.oz.dsto.itd@iris.ucdavis.edu>

We are looking for an ML function which takes an ML string and returns
the corresponding term.  For example:

   `x /\ y` ---> "x /\ y"
   
Is there a quick solution which does not require the use of term
constructors such as mk_const etc?

Any advice will be greatly appreciated.

Tony Cant (email: cant@itd.dsto.oz.au)
Maris Ozols (email: maris@itd.dsto.oz.au)

Trusted Computer Systems Group
Information Technology Division
DSTO
Australia