--- 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