Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id PAA15879; Tue, 21 Nov 1995 15:58:36 +0200
Received: by leopard.cs.byu.edu
	(1.37.109.15/16.2) id AA175696967; Tue, 21 Nov 1995 05:29:27 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Received: from tuminfo2.informatik.tu-muenchen.de by leopard.cs.byu.edu with ESMTP
	(1.37.109.15/16.2) id AA175656948; Tue, 21 Nov 1995 05:29:08 -0700
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <26509-3>; Tue, 21 Nov 1995 13:27:43 +0100
Received: by sunbroy14.informatik.tu-muenchen.de id <8109>; Tue, 21 Nov 1995 13:27:36 +0100
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu, reetz@ira.uka.de
In-Reply-To: <"swan.cl.cam.:242190:951120163440"@cl.cam.ac.uk> (message from Donald Syme on Mon, 20 Nov 1995 16:34:25 +0100)
Subject: Re: better error messages in hol90?
Message-Id: <95Nov21.132736met.8109@sunbroy14.informatik.tu-muenchen.de>
Date: 	Tue, 21 Nov 1995 13:27:23 +0100


> I would like to propose that error messages in hol90 include the term, which
> causes the error. Why? Consider the following situtation: you write a
> function "f",  which, applied to some parameter "p", produces a LARGE term
> and unfortunately, there's a bug in "f" like e.g.
> 
> (f g;()) handle e print_HOL_ERR e;
> 
> Exception raised at Term.list_mk_comb:
> incompatible types
> val it = () : unit

Have you considered using the SML/NJ debugger? I haven't used it, but
tracking down errant exceptions certainly seems to lie in the purview of
debugging.

Konrad.