cosmetics

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 24 16:05:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 24 16:17:30 2010 +0200
@@ -439,10 +439,10 @@
     val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts
 *)
 
-    val need_incremental = Int.max (max_potential, max_genuine) >= 2
-    val effective_sat_solver =
+    val incremental = Int.max (max_potential, max_genuine) >= 2
+    val actual_sat_solver =
       if sat_solver <> "smart" then
-        if need_incremental andalso
+        if incremental andalso
            not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
                        sat_solver) then
           (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
@@ -451,15 +451,14 @@
         else
           sat_solver
       else
-        Kodkod_SAT.smart_sat_solver_name need_incremental
+        Kodkod_SAT.smart_sat_solver_name incremental
     val _ =
       if sat_solver = "smart" then
-        print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^
-                          ". The following" ^
-                          (if need_incremental then " incremental " else " ") ^
-                          "solvers are configured: " ^
-                          commas (map quote (Kodkod_SAT.configured_sat_solvers
-                                                       need_incremental)) ^ ".")
+        print_v (fn () =>
+            "Using SAT solver " ^ quote actual_sat_solver ^ ". The following" ^
+            (if incremental then " incremental " else " ") ^
+            "solvers are configured: " ^
+            commas_quote (Kodkod_SAT.configured_sat_solvers incremental) ^ ".")
       else
         ()
 
@@ -495,9 +494,9 @@
         val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
         val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table
         val min_highest_arity =
-          NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1
+          NameTable.fold (Integer.max o arity_of_rep o snd) rep_table 1
         val min_univ_card =
-          NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table
+          NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table
                          (univ_card nat_card int_card main_j0 [] KK.True)
         val _ = check_arity min_univ_card min_highest_arity
 
@@ -524,15 +523,15 @@
         val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
                       PrintMode.setmp [] multiline_string_for_scope scope
         val kodkod_sat_solver =
-          Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd
+          Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
         val bit_width = if bits = 0 then 16 else bits + 1
-        val delay = if unsound then
-                      Option.map (fn time => Time.- (time, Time.now ()))
-                                 deadline
-                      |> unsound_delay_for_timeout
-                    else
-                      0
-        val settings = [("solver", commas (map quote kodkod_sat_solver)),
+        val delay =
+          if unsound then
+            Option.map (fn time => Time.- (time, Time.now ())) deadline
+            |> unsound_delay_for_timeout
+          else
+            0
+        val settings = [("solver", commas_quote kodkod_sat_solver),
                         ("skolem_depth", "-1"),
                         ("bit_width", string_of_int bit_width),
                         ("symmetry_breaking", signed_string_of_int sym_break),
@@ -731,7 +730,7 @@
         fun print_and_check genuine (j, bounds) =
           print_and_check_model genuine bounds (snd (nth problems j))
         val max_solutions = max_potential + max_genuine
-                            |> not need_incremental ? curry Int.min 1
+                            |> not incremental ? Integer.min 1
       in
         if max_solutions <= 0 then
           (found_really_genuine, 0, 0, donno)

--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Apr 24 16:05:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Apr 24 16:17:30 2010 +0200
@@ -16,6 +16,7 @@
     show_skolems: bool,
     show_datatypes: bool,
     show_consts: bool}
+
   type term_postprocessor =
     Proof.context -> string -> (typ -> term list) -> typ -> term -> term
 

--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Apr 24 16:05:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Sat Apr 24 16:17:30 2010 +0200
@@ -83,7 +83,7 @@
            is_sel s orelse s = @{const_name Sigma} then
           table
         else
-          Termtab.map_default (t, 65536) (curry Int.min (length args)) table
+          Termtab.map_default (t, 65536) (Integer.min (length args)) table
       | aux _ _ table = table
   in aux t [] end
 

--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sat Apr 24 16:05:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sat Apr 24 16:17:30 2010 +0200
@@ -235,7 +235,7 @@
   | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
 (* theory -> (typ option * int list) list -> typ -> int list *)
 fun lookup_type_ints_assign thy assigns T =
-  map (curry Int.max 1) (lookup_ints_assign (type_match thy) assigns T)
+  map (Integer.max 1) (lookup_ints_assign (type_match thy) assigns T)
   handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
          raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
 (* theory -> (styp option * int list) list -> styp -> int list *)

--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Sat Apr 24 16:05:42 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Sat Apr 24 16:17:30 2010 +0200
@@ -324,6 +324,6 @@
   case Kodkod.solve_any_problem false NONE 0 1
                                 (map (problem_for_nut @{context}) tests) of
     Kodkod.Normal ([], _, _) => ()
-  | _ => error "Tests failed"
+  | _ => error "Tests failed."
 
 end;