Added read_def_cterms for simultaneous reading/typing of terms under
defaults.
Redefined read_def_cterm in in terms of read_def_cterms.
Deleted obsolete read_cterms.
Cleaned up def of read_insts, which is not much shorter but much clearere are
correcter now.