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; Tue, 3 Jan 1995 17:04:01 +0000
Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA15407;
          Tue, 3 Jan 1995 09:57:10 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA15403;
          Tue, 3 Jan 1995 09:57:07 -0700
Received: from iraun1.ira.uka.de (iraun1.ira.uka.de [129.13.10.90]) 
          by dworshak.cs.uidaho.edu (8.6.9/1.0) with SMTP id IAA25476 
          for <info-hol@ted.cs.uidaho.edu>; Tue, 3 Jan 1995 08:54:57 -0800
Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP);
          Tue, 3 Jan 1995 17:54:48 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <02533-0@i80fs2.ira.uka.de>;
          Tue, 3 Jan 1995 17:54:48 +0100
To: info-hol@cs.uidaho.edu
Subject: term structure
Date: Tue, 3 Jan 1995 17:54:48 +0100
From: schneide <schneide@ira.uka.de>
Message-Id: <"i80fs2.ira.535:03.01.95.16.54.53"@ira.uka.de>

In the structure TERM, the following data type is declared:

datatype term = Fv of atom
              | Bv of int
              | Const of atom
              | Comb of {Rator : term, Rand : term}
              | Abs of {Bvar : term, Body : term}
              | ty_antiq of Type.hol_type;

The definition of this datatype allows to write functions on terms
with pattern matching. This is not possible with the terms of HOL.
Why can't we have the above type of terms in the HOL system?

Klaus.