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

[Peter Lammich]

> 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.


--
  Peter