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.
