[isabelle-dev] Feedback from a Isabelle tutorial

[Makarius]

On Sun, 26 Jun 2011, Jasmin Christian Blanchette wrote:

> Now, this all sounds well and good, but there is a little glitch. In 
> "try_methods.ML"  the line
>
>    val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose 
> false)
>
> is meant to tell Metis to be quiet, but somehow it is ignored. If you do
>
>    lemma "map f [] = []"
>    using map.simps
>    try_methods
>
> you get the warning
>
>    ### Metis: Unused theorems: "List.map.simps_2"
>
> which is strange because in Metis's code that warning is only printed if 
> "verbose" is true. Is "Proof.map_context" not the thing I should be 
> using?

Proof.map_context is right, also the use of the context later on, as far 
as I can see in the sources.

In fact, I cannot reproduce the above problem in Isabelle/0d78c8d31d0d.


 	Makarius