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; Wed, 7 Jun 1995 14:16:20 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA012498751;
          Wed, 7 Jun 1995 06:39:11 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA012458749;
          Wed, 7 Jun 1995 06:39:09 -0600
Received: from gozo.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP);
          Wed, 7 Jun 1995 13:38:20 +0100
To: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Cc: Clark Barrett <barrett@leopard.cs.byu.edu>, info-hol@leopard.cs.byu.edu, 
    tfm@dcs.gla.ac.uk
Subject: Re: ML/HOL strings
In-Reply-To: Your message of "Wed, 07 Jun 1995 09:55:44 BST." <"swan.cl.cam.:007530:950607085552"@cl.cam.ac.uk>
Date: Wed, 07 Jun 1995 13:38:14 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:143630:950607131812"@cl.cam.ac.uk>

An alternative to 

> let term_for_string s = mk_const (`\`` ^ s ^ `\``,mk_type (`string`,[]));;

is

  let term_for_string = 
      let ty = mk_type (`string`,[]) in
          \s. mk_const (`\`` ^ s ^ `\``,);;

This avoids rebuilding ":string" each time it's called.  On the other
hand, it's undefinable until the string library has been loaded...

Tom