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 XAA19608; Tue, 6 Feb 1996 23:56:18 +0200
Received: by leopard.cs.byu.edu
	(1.37.109.15/16.2) id AA073989825; Tue, 6 Feb 1996 13:50:25 -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 AA073909805; Tue, 6 Feb 1996 13:50:05 -0700
Received: by tuminfo2.informatik.tu-muenchen.de via suspension id <26639-4>; Tue, 6 Feb 1996 21:47:15 +0100
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <26999-4>; Tue, 6 Feb 1996 17:34:24 +0100
Received: by sunbroy14.informatik.tu-muenchen.de id <8161>; Tue, 6 Feb 1996 17:18:48 +0100
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu, reetz@ira.uka.de, schneide@ira.uka.de
Subject: Re: How do I get the definition of a constant in HOL90?
Message-Id: <96Feb6.171848met.8161@sunbroy14.informatik.tu-muenchen.de>
Date: 	Tue, 6 Feb 1996 17:18:35 +0100


Actually, one doesn't have to go through the rigamarole about dropping
dollar signs, since that's also surface syntax. Sorry about that!

(* Revised version *)
fun find_def s =
  let val {theory,...} = const_decl s
      fun our_const c = (#Name(dest_const c) = s) handle _ => false
  in first (can (find_term our_const) o concl o #2) 
           (rev(definitions theory))
  end;