Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 14 Jun 1995 12:21:47 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA003924373;
          Wed, 14 Jun 1995 04:06:13 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from iraun1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA003013719;
          Wed, 14 Jun 1995 03:55:19 -0600
Received: from i80fs1.ira.uka.de by iraun1.ira.uka.de with SMTP (PP);
          Wed, 14 Jun 1995 10:01:49 +0200
Received: from ira.uka.de by i80fs1.ira.uka.de id <03464-0@i80fs1.ira.uka.de>;
          Wed, 14 Jun 1995 10:01:36 +0200
Date: Wed, 14 Jun 95 9:59:19 EDT
From: 0000-Admin (0000) <root@ira.uka.de>
To: info-hol@leopard.cs.byu.edu
Cc: slind@informatik.tu-muenchen.de, reetz@ira.uka.de
Subject: RE: Problems with loading a theory - don't use `=' in a theory name
Message-Id: <"i80fs1.ira.466:14.06.95.08.01.42"@ira.uka.de>

Concerning previous message to info-hol:

I found the problem: I accidently used `=' in a theory name, i.e. I had

val _ = save_thm("foo=",prove(--` ...
                     ^
                     |
                   look here

the function save_thm did accept the `=' in the theory name, but the
parser invoked during loading the theory from disk crashed.

So I would like to suggest that either save_thm does not accept
theory names with a `=' or that the parser should be changed to
accept `=' in a theory name. Otherwise, bugging not that fun (as
I found out...)

cheers, Ralf