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; Thu, 19 May 1994 12:30:37 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA25535;
          Thu, 19 May 1994 05:15:10 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from tuminfo2.informatik.tu-muenchen.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA25531;
          Thu, 19 May 1994 05:14:45 -0600
Received: by tuminfo2.informatik.tu-muenchen.de via suspension id <326553>;
          Thu, 19 May 1994 13:14:54 +0200
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <326559>;
          Thu, 19 May 1994 13:14:22 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8067>;
          Thu, 19 May 1994 13:13:55 +0200
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: reetz@ira.uka.de, info-hol@leopard.cs.byu.edu
Subject: Re: converting hol-types to string in hol90.6
Message-Id: <94May19.131355met_dst.8067@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 19 May 1994 13:13:48 +0200


> I wonder about how to convert a hol-type into a string of sml in hol90.6
> based on NJ/SML 0.93. 

"type_to_string" and "term_to_string" are already provided in hol90.6,
in the structure Hol_pp, and are implemented in the way Ralph described: 

    (* Ad-hoc combinator to permute arguments *)
    fun P f x y z = f y z x;

    fun type_to_string ty =
       PP.pp_to_string (!Globals.linewidth) 
                       (P pp_type (!Globals.max_print_depth))
                       ty;

    fun term_to_string tm = PP.pp_to_string (!Globals.linewidth) pp_term tm


Konrad.