give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;