a lot of changes in refine; new method 'sample WitnessSet' (takes Tolerance option)