removed eq_sg, pprint_sg, print_sg (now in sign.ML); removed cterm_fun, read_ctyp (now in thm.ML); print_theory: now shows all contents;