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; Sun, 12 Dec 1993 23:02:29 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26465; Sun, 12 Dec 1993 15:47:56 -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 AA26461; Sun, 12 Dec 1993 15:47:32 -0700 Received: from tuminfo2.informatik.tu-muenchen.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA15521; Sun, 12 Dec 1993 14:45:20 -0800 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <57654>; Sun, 12 Dec 1993 23:45:00 +0100 Received: by sunbroy14.informatik.tu-muenchen.de id <8097>; Sun, 12 Dec 1993 23:44:43 +0100 From: Konrad Slind To: info-hol@cs.uidaho.edu, schneide@ira.uka.de, reetz@ira.uka.de Subject: strange rewrite Message-Id: <93Dec12.234443met.8097@sunbroy14.informatik.tu-muenchen.de> Date: Sun, 12 Dec 1993 23:44:28 +0100 Klaus Schneider asks: > Can anyone explain this strange behaviour of REWRITE_TAC?? The problem can be traced to the "subst" primitive. A simple example demonstrating the bug is val tm = --`\(p:'a) (q:'a). f (x:'a) (y:'a) : 'a`--; val theta = [{redex = --`x:'a`--, residue = --`q:'a`--}, {redex = --`y:'a`--, residue = --`p:'a`--}]; subst theta tm; The answer should be the term \p' q'. f q p but hol90.6 fails with a CLASH error. This bug is "conservative", in that it can not be used to prove |- F; it just raises an exception in a case where it ought to rename and proceed. The bug has been fixed; the fix can be ftp'ed from Munich: machine = ftp.informatik.tu-muenchen.de file = local/lehrstuhl/nipkow/hol90/patch2.tar.Z Konrad.