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, 1 Dec 1992 17:05:02 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA10215;
          Tue, 1 Dec 92 08:38:45 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from [130.89.10.247] by ted.cs.uidaho.edu (16.6/1.34) id AA10210;
          Tue, 1 Dec 92 08:38:22 -0800
Received: from apollo.cs.utwente.nl by utrhcs.cs.utwente.nl (4.1/RBCS-2.3mx) 
          id AA12754; Tue, 1 Dec 92 17:37:09 +0100
Received: from highschool.cs.utwente.nl by apollo.cs.utwente.nl (4.1/RBCS-2.0) 
          id AA07134; Tue, 1 Dec 92 17:37:05 +0100
Date: Tue, 1 Dec 92 17:37:05 +0100
From: blok@nl.utwente.cs (Rintcius Blok)
Message-Id: <9212011637.AA07134@apollo.cs.utwente.nl>
To: info-hol@edu.uidaho.cs.ted
Subject: recursive def. problem

Hello,

I have a problem with defining a simple looking function. I just
want to write a recursive function based on the type (*)ltree,
that returns the root of a ltree.
I tried the following definition:

#new_recursive_definition false ltree_Axiom
#  `GetTop`
#  "GetTop (Node (top:*) desc) = top";;

HOL answered with:

Badly typed application of:  "GetTop"
   which has type:           ":(*)ltree -> *"
to the argument term:        "desc"
   which has type:           ":((*)ltree)list"

evaluation failed     Can't solve recursion equation: Can't instantiate existence theorem

I think it has something to do with the fact that the 
type definition package is based on trees, but I cannot find a
solution.
Does someone know how to solve my problem?

Thanks,
Rintcius.