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 OAA23542; Tue, 10 Oct 1995 14:36:15 +0200
Received: by leopard.cs.byu.edu
	(1.37.109.15/16.2) id AA196582778; Tue, 10 Oct 1995 04:59:38 -0600
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with ESMTP
	(1.37.109.15/16.2) id AA196552777; Tue, 10 Oct 1995 04:59:37 -0600
Received: from vanuata.dcs.gla.ac.uk (vanuata.dcs.gla.ac.uk [130.209.240.50]) by dworshak.cs.uidaho.edu (8.6.12/1.1) with ESMTP id DAA12318 for <info-hol@cs.uidaho.edu>; Tue, 10 Oct 1995 03:59:15 -0700
Message-Id: <199510101059.DAA12318@dworshak.cs.uidaho.edu>
Received: from malta.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk 
          with LOCAL SMTP (PP); Tue, 10 Oct 1995 11:56:27 +0100
To: shaw@cs.ucdavis.edu (Rob Shaw)
Cc: info-hol@cs.uidaho.edu, tfm@dcs.gla.ac.uk
Subject: Re: ACCEPT_TAC nit pick... 
In-Reply-To: Your message of "Mon, 09 Oct 1995 16:54:52 PDT."             <199510092354.QAA19306@roma-cafe.cs.ucdavis.edu> 
Date: Tue, 10 Oct 1995 11:56:01 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>


> Hi, why does HOL90 behave in the following way? (not giving you your actual
>goal term as the resulting theorem, but rather the thm you gave to ACCEPT_TAC)

HOL88 was revised years ago to behave as you want (see attached extract
from the source files).  Maybe the modification didn't make it into HOL90?

Tom

% --------------------------------------------------------------------- %
% Revised to return a theorem alpha-identical to goal.  [TFM 93.07.22]  %
% OLD CODE:                                                             %
%                                                                       %
% let ACCEPT_TAC th :tactic (asl,w) =                                   %
%     if aconv (concl th) w then [], \[].th                             %
%     else failwith `ACCEPT_TAC`;;                                      %
% --------------------------------------------------------------------- %

let ACCEPT_TAC th :tactic (asl,w) =
    if aconv (concl th) w then 
       [], \[]. EQ_MP (ALPHA (concl th) w) th
    else failwith `ACCEPT_TAC`;;