tuning

rename

use "Metis_" prefix rather than "Metis" structure; the prefix can then be used not only for structures but also signatures and functors. A few other changes were made to the script, to eliminate the need for "metis_env.ML".

no need for TPTP

put "foldl" and "foldr" in "Useful"; Isabelle hides those symbols from List, but by adding them to Useful we have them throughout Metis without "List." prefix

reintroduce the CRITICAL sections from change 3880d21d6013

apply Larry's hacks directly to the "src" files; these hacks modify the defaults of Metis heuristics and are necessary for backward compatibility