Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 7 Jun 1995 10:23:00 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA278205337; Wed, 7 Jun 1995 02:55:37 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA278155322; Wed, 7 Jun 1995 02:55:22 -0600 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 7 Jun 1995 09:55:47 +0100 To: Clark Barrett Cc: info-hol@leopard.cs.byu.edu, Richard.Boulton@cl.cam.ac.uk Subject: Re: ML/HOL strings In-Reply-To: Your message of "Tue, 06 Jun 1995 11:48:28 MDT." <199506061748.AA276750909@cheetah.cs.byu.edu> Date: Wed, 07 Jun 1995 09:55:44 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:007530:950607085552"@cl.cam.ac.uk> Clark Barrett writes: > 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? You appear to be using HOL88, so I think the function you require can be defined as follows: let term_for_string s = mk_const (`\`` ^ s ^ `\``,mk_type (`string`,[]));; Richard Boulton