[isabelle-dev] "local_setup" and "Generic_Data"

[Jasmin Christian Blanchette]

Hi all,

> I was trying to make Nitpick more context-friendly and thought that "local_setup" and "Generic_Data" would be my friends. However, "local_setup" seems to do nothing -- the changes I perform to the data are coldly ignored. The little theory below shows illustrates what I mean:
> [...]
> local_setup {* Context.proof_map (Data.map (Integer.add 3)) *}

FYI. Florian has explained this to me live. For the record,

    local_setup {* Local_Theory.target (Context.proof_map (Data.map (Integer.add 3))) *}

or

    declaration {* fn phi => Data.map (Integer.add 3) *}

do the trick.

Jasmin