diff -r 76d5fd5a45fb -r ff5f88702590 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sat Apr 24 16:17:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Sat Apr 24 16:33:01 2010 +0200
@@ -51,8 +51,6 @@
    ("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
                             "s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
 
-(* string -> sink -> string -> string -> string list -> string list
-   -> (string * (unit -> string list)) option *)
 fun dynamic_entry_for_external name dev home exec args markers =
   case getenv home of
     "" => NONE
@@ -74,8 +72,6 @@
                       if dev = ToFile then out_file else ""] @ markers @
                       (if dev = ToFile then [out_file] else []) @ args
                    end)
-(* bool -> bool -> string * sat_solver_info
-   -> (string * (unit -> string list)) option *)
 fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
     if incremental andalso mode = Batch then NONE else SOME (name, K ss)
   | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
@@ -98,20 +94,15 @@
         (name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
     dynamic_entry_for_external name dev home exec args [m1, m2, m3]
   | dynamic_entry_for_info true _ = NONE
-(* bool -> (string * (unit -> string list)) list *)
 fun dynamic_list incremental =
   map_filter (dynamic_entry_for_info incremental) static_list
 
-(* bool -> string list *)
 val configured_sat_solvers = map fst o dynamic_list
-(* bool -> string *)
 val smart_sat_solver_name = fst o hd o dynamic_list
 
-(* string -> string * string list *)
 fun sat_solver_spec name =
   let
     val dyn_list = dynamic_list false
-    (* (string * 'a) list -> string *)
     fun enum_solvers solvers =
       commas (distinct (op =) (map (quote o fst) solvers))
   in