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, 9 Dec 1993 16:46:01 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26708;
          Thu, 9 Dec 1993 09:33:31 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA26704;
          Thu, 9 Dec 1993 09:33:16 -0700
Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA03359;
          Thu, 9 Dec 1993 08:29:51 -0800
Received: from ira.uka.de by iraun1.ira.uka.de id <12873-0@iraun1.ira.uka.de>;
          Thu, 9 Dec 1993 17:29:22 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <15003-0@i80fs2.ira.uka.de>;
          Thu, 9 Dec 1993 17:28:27 +0100
Date: Thu, 9 Dec 93 17:28:26 EST
From: reetz <reetz@ira.uka.de>
To: info-hol@cs.uidaho.edu
Cc: schneide@ira.uka.de
Subject: define_type within hol90.5 and hol90.6
Message-Id: <"i80fs2.ira.005:09.11.93.16.28.29"@ira.uka.de>

Dear all,
the following did work fine in hol90.5:

new_theory "demo";

define_type
  {fixities =[Prefix,Prefix,Prefix],
   name     ="CompTree",
   type_spec=`CompTree=C_Compnode  of CompTree#CompTree#('M->'M->'M)|
                       C_Varleaf   of 'VN|
                       C_Constleaf of 'M`};

using hol90.6, I get the following:

define_type
  {fixities =[Prefix,Prefix,Prefix],
   name     ="CompTree",
   type_spec=`CompTree=C_Compnode  of CompTree#CompTree#('M->'M->'M)|
                       C_Varleaf   of 'VN|
                       C_Constleaf of 'M`};

Exception raised at Parse_support.make_type_clause.check:
recursive occurrence of defined type is deeper than the first level
 
uncaught exception HOL_ERR

does anybody have an idea?

thanks in advance :)
(*****************************************************************************)
(*                                                                           *)
(*  Ralf Reetz                 SFB 358 of the german research society (DFG)  *)
(*  reetz@ira.uka.de           University of Karlsruhe, Germany              *)
(*                                                                           *)
(*                "we prove around in a ring and suppose,                    *)
(*                 the goal sits right in the middle and knows."             *)
(*                                                                           *)
(*****************************************************************************)