[isabelle-dev] Speed of @{thm}

[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?

The experimentation with Poly/ML compiler characteristics can be made more 
efficient by showing David Matthews some reproducible examples.


 	Makarius