[isabelle-dev] Quick and dirty update of theory ?

[Steven Obua]

Hi,

I have the following setup:

(1) a theory "lemmas.thy"
(2) some ML-code that uses this theory and that is loaded and executed 
after the theory has been loaded
(3) some additional ML-code that defines a function f

I now use f and suddenly I notice that I have to update lemmas.thy by 
for example adding another lemma to it (I dont take anything out of the 
theory, but just add to it). Reloading lemmas.thy via 'use_thy "lemmas"' 
works. But then a call to the function f returns the error message

*** Exception- ERROR "Different versions of theory component \"lemmas\""
***    raised

well, that is to be expected, but reloading (2) costs me about 15 
minutes (and raising), but is not really necessary. Does anybody know of 
some hack (possibly in connection with the quick_n_dirty flag) to 
circumvent above error message ?

Steven