src/Pure/Isar/proof.ML

   val assert_forward_or_chain: state -> state
   val assert_backward: state -> state
   val assert_no_chain: state -> state
   val enter_forward: state -> state
   val verbose: bool ref
+  val show_main_goal: bool ref
   val pretty_state: int -> state -> Pretty.T list
   val pretty_goals: bool -> state -> Pretty.T list
   val level: state -> int
   type method
   val method: (thm list -> tactic) -> method

 
 
 
 (** pretty_state **)
 
+val show_main_goal = ref true;
+
 val verbose = ProofContext.verbose;
 
 fun pretty_goals_local ctxt = Display.pretty_goals_aux
   (ProofContext.pretty_sort ctxt, ProofContext.pretty_typ ctxt, ProofContext.pretty_term ctxt);
 

     fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) =
       pretty_facts "using " ctxt
         (if mode <> Backward orelse null goal_facts then None else Some goal_facts) @
       [Pretty.str ("goal (" ^ kind_name (sign_of state) kind ^ prt_names names ^
           levels_up (i div 2) ^ subgoals (Thm.nprems_of thm) ^ "):")] @
-      pretty_goals_local ctxt begin_goal (true, true) (! Display.goals_limit) thm;
+      pretty_goals_local ctxt begin_goal (true, !show_main_goal) (! Display.goals_limit) thm;
 
     val ctxt_prts =
       if ! verbose orelse mode = Forward then ProofContext.pretty_context ctxt
       else if mode = Backward then ProofContext.pretty_asms ctxt
       else [];

     fun err msg = raise STATE (msg, state);
 
     val ngoals = Thm.nprems_of raw_th;
     val _ =
       if ngoals = 0 then ()
-      else (err (Pretty.string_of (Pretty.chunks (pretty_goals_local ctxt "" (true, true)
+      else (err (Pretty.string_of (Pretty.chunks (pretty_goals_local ctxt "" (true, !show_main_goal)
             (! Display.goals_limit) raw_th @
           [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))));
 
     val {hyps, sign, ...} = Thm.rep_thm raw_th;
     val tsig = Sign.tsig_of sign;