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 BAA27890; Sat, 13 Jan 1996 01:17:42 +0200
Received: by leopard.cs.byu.edu
	(1.37.109.15/16.2) id AA168173670; Fri, 12 Jan 1996 14:54:30 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Received: from jaguar.cs.byu.edu by leopard.cs.byu.edu with ESMTP
	(1.37.109.15/16.2) id AA168133669; Fri, 12 Jan 1996 14:54:29 -0700
From: "Paul E. Black" <black@leopard.cs.byu.edu>
Received: by jaguar.cs.byu.edu (1.37.109.15/CS-Client)
	id AA175523581; Fri, 12 Jan 1996 14:53:01 -0700
Date: Fri, 12 Jan 1996 14:53:01 -0700
Message-Id: <199601122153.AA175523581@jaguar.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: general renaming

I need to rename (free) variables in theorems, eg,
	|- a = b
into
	|- a = c

Is there function in HOL88 which does this?  I can see
how to write more own with a few functions, but I
wanted to reuse if possible.

-paul-