[isabelle] Storing data in a locale

Dear all,

I am trying to store some data in the context of a locale which I can
later extract when working in that particular locale.

I thought I could use Proof_Data and local_setup as illustrated in the 
following code snippet: 

structure Numbs = Proof_Data(type T = int fun init _ =  1);
val set_numbs = Numbs.map o K;
val get_numbs = Numbs.get;

locale test
 local_setup{* set_numbs 2 *}

lemma (in test) "True"
 ML_prf{* get_numbs @{context} *}

However, get_numbs returns (the initial) 1 and not 2 as I would expect.

Does anyone know how I can achieve this?



The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.