ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;

merged

tuned code

quotient package: deal correctly with frees in lifted theorems

approximation_oracle: actually match true/false in ML, not arbitrary values;

renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;

more precise Command.State accumulation;