[isabelle-dev] Speed of @{thm}

[Jasmin Blanchette]

Am 11.08.2012 um 23:44 schrieb Makarius:

> On Fri, 10 Aug 2012, Jasmin Blanchette wrote:
> 
>> Now, here's something really strange. If I replace
>> 
>>   fun thm_bind kind a i =
>>     "val " ^ a ^ " = the_" ^ kind ^
>>       " (ML_Context.the_local_context ()) " ^ string_of_int i ^ ";\n";
>> 
>> with
>> 
>>   fun my_ctxt () = ML_Context.the_local_context ();
>> 
>>   fun thm_bind kind a i =
>>     "val " ^ a ^ " = the_" ^ kind ^
>>       " (my_ctxt ()) " ^ string_of_int i ^ ";\n";
>> 
>> then things get 10 times faster (at least on my copy of "ml_thms.ML", all within the "ML {* *}" tags of a ".thy" file). The truth must be hidden somewhere in "ml_context.ML".
> 
> 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.

Jasmin