[isabelle-dev] Advice for replacing @{simpset} with @{context}.

[Makarius]

On Fri, 13 Sep 2013, Peter Lammich wrote:

>> The relevant text from NEWS is this:
>>
>> * Simplifier tactics and tools use proper Proof.context instead of
>> historic type simpset.  Old-style declarations like addsimps,
>> addsimprocs etc. operate directly on Proof.context.  Raw type simpset
>> retains its use as snapshot of the main Simplifier context, using
>> simpset_of and put_simpset on Proof.context.  INCOMPATIBILITY -- port
>> old tools by making them depend on (ctxt : Proof.context) instead of
>> (ss : simpset), then turn (simpset_of ctxt) into ctxt.
>>
>
> So the only way to replace a "HOL_basic_ss addsimps ..." somewhere deep
> inside my code (in my actual case, inside a conversion) is to thread
> through the proof context everywhere? ... a quite tedious change.

Is this hypothetical, or do you still have tools without a proper context?

It should be trivial to pass through some ctxt: Proof.context nonetheless, 
i.e. do the "localization" in that elementary sense.  Unless there is 
something really strange here ...


 	Makarius