(* $Id$ *) setmp_noncritical print_mode (! print_mode @ ["no_brackets", "no_type_brackets"]) use_thy "Unix";