[isabelle-dev] Speed of @{thm}

[Makarius]

On Sun, 12 Aug 2012, Jasmin Blanchette wrote:

>> Reading this again, I don't understand it.  Which detail made the 
>> difference?
>
> Creating a "my_ctxt" function that indirectly called 
> "ML_Context.the_local_context". But I haven't tried this in Isabelle, 
> only in my mock-up theory.

Never mind.  I have yet another refinement in the pipeline, so in a minute 
the problem might actually be solved.


 	Makarius