src/HOL/Tools/Sledgehammer/sledgehammer_print.ML

     | _ =>*) (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
             of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
             of_indent 0 ^ (if n <> 1 then "next" else "qed")
   end
 
-end
+end;