src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

                 s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
               | _ => fold (curry s_disj) lits @{term False})
             end
             |> HOLogic.mk_Trueprop |> finish_off
 
-        fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show
+        fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else []
 
         fun isar_steps outer predecessor accum [] =
             accum
             |> (if tainted = [] then
+                  (* e.g., trivial, empty proof by Z3 *)
                   cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
                     sort_facts (the_list predecessor, []), massage_methods systematic_methods', ""))
                 else
                   I)
             |> rev

                  else if is_arith_rule rule then arith_methods
                  else if is_datatype_rule rule then datatype_methods
                  else systematic_methods')
                 |> massage_methods
 
-              fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "")
+              fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "")
               fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs
             in
               if is_clause_tainted c then
                 (case gamma of
                   [g] =>

                 isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
               val c = succedent_of_cases cases
               val l = label_of_clause c
               val t = prop_of_clause c
               val step =
-                Prove (maybe_show outer c [], [], l, t,
+                Prove (maybe_show outer c, [], l, t,
                   map isar_case (filter_out (null o snd) cases),
                   sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")
             in
               isar_steps outer (SOME l) (step :: accum) infs
             end

           refute_graph
           |> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
           |> redirect_graph axioms tainted bot
           |> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
           |> isar_proof true params assms lems
+          |> postprocess_isar_proof_remove_show_stuttering
           |> postprocess_isar_proof_remove_unreferenced_steps I
           |> relabel_isar_proof_canonically
 
         val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof