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 07:45:40 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA271140511;
          Wed, 14 Jun 1995 00:15:11 -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 AA270990492;
          Wed, 14 Jun 1995 00:14:52 -0600
Received: from i80fs1.ira.uka.de by iraun1.ira.uka.de with SMTP (PP);
          Wed, 14 Jun 1995 08:15:23 +0200
Received: from ira.uka.de by i80fs1.ira.uka.de id <03227-0@i80fs1.ira.uka.de>;
          Wed, 14 Jun 1995 08:15:12 +0200
Date: Wed, 14 Jun 95 8:12:56 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: Problems with loading a theory in HOL90.7
Message-Id: <"i80fs1.ira.229:14.06.95.06.15.16"@ira.uka.de>

To:info-hol@lal.cs.byu.edu
cc:slind@informatik.tu-muenchen.de, schneide, reetz
Subject:
--------
I have a `strange' problem with hol90.7:

1.) I built a library, which included making theories "ct",
    "ctrl", "fgm".
    Successful.
2.) I restarted hol, load this library.
    Successful.
3.) I executed `html_theory "ct"' and `html_theory "ctrl".
    Successful.
4.) I executed `html_theory "fgm"' and I got:
=========
thms parser error: syntax error
 
 
found "/opt/hol/contrib/fgm/theories/ascii/fgm.thms" 
but couldn't read it successfully: continuing
 
uncaught exception HOL_ERR
=========
more precisely with print_HOL_ERR:
=========
thms parser error: syntax error
 
 
found "/opt/hol/contrib/fgm/theories/ascii/fgm.thms"
but couldn't read it successfully: continuing
 
Exception raised at File.get_file_by_key:
unable to get the file "fgm.thms"
===========
I checked the permissions, the file ..../fgm.thms. It 
looked o.k. I have done that procedure
`I-can-not-count-anymore' times and it always worked that
way. I rebuilt everything in the proper order, so
timestamps in the theory files should be o.k. The only
thing that is different is a minor change in the theory
"fgm". However, theory "fgm" was made sucessfully.

I really can't figure out what is wrong here. Has
somebody any hint for me what is happen here?

Thanks in advance a lot!

Ralf.

(*******************************************************************)
(*                                                                 *)
(*  Ralf Reetz                                                     *)
(*                                                                 *)
(*  University of Karlsruhe                                        *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz                *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany              *)
(*                                                                 *)
(*  e-mail: reetz@informatik.uni-karlsruhe.de or reetz@ira.uka.de  *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html       *)
(*  fax:    +49 721 370455                                         *)
(*  tel:    +49 721 6083771                                        *)
(*                                                                 *)
(*******************************************************************)