src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

                      in
                        ((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
                      end)
                  else
                    one_line_params) ^
-              (if isar_proofs = SOME true then "\n(No Isar proof available.)" else "")
+              (if isar_proofs = SOME true then "\n(No Isar proof available)" else "")
             | (_, num_steps) =>
               let
                 val msg =
                   (if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps]
                    else []) @