consts: maintain thy version for efficient transfer;
ins_sorts: Vartab.replace is slower than Vartab.update, but might avoid some copying of table structure;
use "../settings.ML";no_document use_thy "While_Combinator";use_thy "simp";use_thy "WFrec";use_thy "Partial";