[isabelle-dev] copying contexts

[Lucas Dixon]

Hello,

I'm wondering what the right way to copy contexts is. I remember there
was some references lingering in theories, mostly as unique identifies
if I remember correctly, but it meant that copying needed to be an
explicit function. Is this the right way to copy a context:

Context.map_theory Context.copy_thy

and so copying a proof context would be:

Context.proof_map (Context.map_theory Context.copy_thy)

?

The reason I want to do this is that when proof planning proves new
theorems it creates some meta-data which gets stored in the context. I
want to be able to make a copy the context before I modify any such data
so that I can compare alternatives and do fair tests. I was previously
using my own generic context, but would like to cut down code duplication.

cheers,
lucas

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