# HG changeset patch
# User blanchet
# Date 1504821745 -7200
# Node ID e3dccf7725a380d747609e9c9a0f724786e020c9
# Parent  2cd22f0709293b272727a5819aa61380d6c49d5f
repaired Nunchaku cache handing

diff -r 2cd22f070929 -r e3dccf7725a3 src/HOL/Tools/Nunchaku/nunchaku_tool.ML
--- a/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:02:24 2017 +0200
+++ b/src/HOL/Tools/Nunchaku/nunchaku_tool.ML	Fri Sep 08 00:02:25 2017 +0200
@@ -82,7 +82,7 @@
 val unknown_solver = "unknown";
 
 val cached_outcome = Synchronized.var "Nunchaku_Tool.cached_outcome"
-  (NONE : ((string list * nun_problem) * nun_outcome) option);
+  (NONE : ((tool_params * nun_problem) * nun_outcome) option);
 
 fun uncached_solve_nun_problem
     ({solvers, overlord, initial_bound, bound_increment, specialize, timeout, ...} : tool_params)
@@ -136,7 +136,7 @@
       end);
 
 fun solve_nun_problem (params as {solvers, overlord, debug, ...}) problem =
-  let val key = (solvers, problem) in
+  let val key = (params, problem) in
     (case (overlord orelse debug,
         AList.lookup (op =) (the_list (Synchronized.value cached_outcome)) key) of
       (false, SOME outcome) => outcome