Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Tue, 8 Sep 1992 18:55:24 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15478;
          Tue, 8 Sep 92 09:52:17 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from grolsch.cs.ubc.ca by ted.cs.uidaho.edu (16.6/1.34) id AA15473;
          Tue, 8 Sep 92 09:51:57 -0700
Received: by grolsch.cs.ubc.ca id AA14179 (5.65c/IDA-1.3.5 
          for info-hol@ted.cs.uidaho.edu); Tue, 8 Sep 1992 09:50:43 -0700
Date: 8 Sep 92 9:50 -0700
From: Sreeranga Rajan <sree@ca.ubc.cs>
To: vdvoort <vdvoort@nl.utwente.cs>
Cc: info-hol@edu.uidaho.cs.ted
Message-Id: <609*sree@cs.ubc.ca>
Subject: Re: short query

In reply to Mark's (vdvoort@cs.utwente.nl) message:

Thanks. But, the problem lies in identifying the theorem associated with
define_type - which introduces the type constructors.
So, my query was - is there a better way than a naming convention
for this identification?
The reason for separating the constructors, is that I need to treat them
separately in my ML program.
Regards,
	-Sree