Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <09130-0@swan.cl.cam.ac.uk>; Thu, 31 Oct 1991 14:28:27 +0000
Received: by ted.cs.uidaho.edu (15.11/1.34) id AA04287;
          Thu, 31 Oct 91 06:17:52 pst
Reply-To: info-hol@ted
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@ted.cs.uidaho.edu
Received: from [128.232.0.56] by ted.cs.uidaho.edu (15.11/1.34) id AA04282;
          Thu, 31 Oct 91 06:17:12 pst
Received: from guillemot.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP) to cl
          id <08769-0@swan.cl.cam.ac.uk>; Thu, 31 Oct 1991 14:08:35 +0000
To: info-hol@edu.uidaho.cs.ted
Cc: Tom.Melham@uk.ac.cam.cl
Subject: autoloading and compilation (HOL88).
Date: Thu, 31 Oct 91 14:08:32 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.771:31.09.91.14.08.37"@cl.cam.ac.uk>


HOL users may be interested in the following question and its answer.

Q: I have recently had a few problems using autoloaded theorem names in
   compiled code. Generally it seems to work, but sometimes the compiled code
   fails to load with a complaint that the theorem is undefined (the failure
   cannot reliably be repeated). Is this supposed to work?

A: Yes, mentioning autoload names in code to be compiled can be a problem.
   What I always do is the following.  Suppose you have a function:

      let fun x =  ... THM ...

   where THM is the autoload name of some built-in theorem, and you wish
   to compile this function.  A thing that works is to do:

      let fun =
          let thm = theorem `thy` `THM` in
          \x. ... thm ...

   where thm is NOT the autoload name of anything.  You can then compile
   fun without deactivating the autoloading of THM.

Tom