# HG changeset patch
# User blanchet
# Date 1355315281 -3600
# Node ID 0b7288aee7514e9a7f8252be8306133216dabfa5
# Parent  1b3eb579e08b481e7a416e01e9015305ed7309d3
tuning

diff -r 1b3eb579e08b -r 0b7288aee751 src/HOL/Tools/Nitpick/kodkod_sat.ML
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Dec 12 11:56:07 2012 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML	Wed Dec 12 13:28:01 2012 +0100
@@ -106,16 +106,16 @@
 
 fun sat_solver_spec name =
   let
-    val dyn_list = dynamic_list false
+    val dyns = dynamic_list false
     fun enum_solvers solvers =
       commas (distinct (op =) (map (quote o fst) solvers))
   in
-    (name, the (AList.lookup (op =) dyn_list name) ())
+    (name, the (AList.lookup (op =) dyns name) ())
     handle Option.Option =>
            error (if AList.defined (op =) static_list name then
                     "The SAT solver " ^ quote name ^ " is not configured. The \
                     \following solvers are configured:\n" ^
-                    enum_solvers dyn_list ^ "."
+                    enum_solvers dyns ^ "."
                   else
                     "Unknown SAT solver " ^ quote name ^ ". The following \
                     \solvers are supported:\n" ^ enum_solvers static_list ^ ".")