# HG changeset patch
# User wenzelm
# Date 1597953388 -7200
# Node ID 13dc5fe14a49a8c701efec43f828146fd4ac575f
# Parent  1337904169d7f54edceac4c6c28c452c5af3a428
tuned;

diff -r 1337904169d7 -r 13dc5fe14a49 src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Thu Aug 20 16:00:59 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Thu Aug 20 21:56:28 2020 +0200
@@ -861,12 +861,12 @@
                else
                  "int_bounds: " ^
                  commas (map int_string_for_bound int_bounds) ^ "\n"));
-         map (fn b => (out_assign b; out ";")) expr_assigns;
+         List.app (fn b => (out_assign b; out ";")) expr_assigns;
          out "solve "; out_outmost_f formula; out ";\n")
   in
     out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
          "// " ^ ATP_Util.timestamp () ^ "\n");
-    map out_problem problems
+    List.app out_problem problems
   end
 
 (** Parsing of solution **)
@@ -1021,7 +1021,7 @@
         val _ = File.write_buffer in_path (!in_buf)
         fun remove_temporary_files () =
           if overlord then ()
-          else List.app (K () o try File.rm) [in_path, out_path, err_path]
+          else List.app (ignore o try File.rm) [in_path, out_path, err_path]
       in
         let
           val ms = milliseconds_until_deadline deadline