Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 21 Dec 1993 11:09:46 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03751; Tue, 21 Dec 1993 04:02:10 -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 AA03747; Tue, 21 Dec 1993 04:02:05 -0700 Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA16177; Tue, 21 Dec 1993 03:00:07 -0800 Received: from skua.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 21 Dec 1993 10:59:47 +0000 To: Wishnu Prasetya Cc: info-hol@cs.uidaho.edu (hol mailing list), Wai.Wong@cl.cam.ac.uk Subject: Re: Help with DEPTH_CONV In-Reply-To: Your message of "Tue, 21 Dec 93 11:35:27 +0100." <199312211035.AA08606@relay.cs.ruu.nl> Date: Tue, 21 Dec 93 10:59:39 +0000 From: Wai Wong Message-Id: <"swan.cl.cam.:108460:931221105953"@cl.cam.ac.uk> Wishnu, The problem you have is not the size of the subterms, but the conversion can be applied to the subterm REPEATEDLY. This means the system drops in an infinite loop. As the manual page says: DEPTH_CONV c tm repeatedly applies the conversion c to all the subterms of the term tm, including the term tm itself. The supplied conversion is applied repeatedly (zero or more times, as is done by REPEATC) to each subterm until it fails. You should use ONCE_DEPTH_CONV instead of DEPTH_CONV in this case. Wai