# HG changeset patch
# User haftmann
# Date 1475498070 -7200
# Node ID 789f5419926a115933236ff363f91d2f00ce0c17
# Parent  54b785efd547412f446e565edb5c772fee0f6500
modernized option

diff -r 54b785efd547 -r 789f5419926a src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Mon Oct 03 14:34:29 2016 +0200
+++ b/src/Tools/solve_direct.ML	Mon Oct 03 14:34:30 2016 +0200
@@ -14,7 +14,7 @@
   val someN: string
   val noneN: string
   val unknownN: string
-  val max_solutions: int Unsynchronized.ref
+  val max_solutions: int Config.T
   val solve_direct: Proof.state -> bool * (string * string list)
 end;
 
@@ -32,7 +32,7 @@
 
 (* preferences *)
 
-val max_solutions = Unsynchronized.ref 5;
+val max_solutions = Attrib.setup_config_int @{binding solve_direct_max_solutions} (K 5);
 
 
 (* solve_direct command *)
@@ -44,7 +44,8 @@
 
     val crits = [(true, Find_Theorems.Solves)];
     fun find g =
-      snd (Find_Theorems.find_theorems find_ctxt (SOME g) (SOME (! max_solutions)) false crits);
+      snd (Find_Theorems.find_theorems find_ctxt (SOME g)
+        (SOME (Config.get find_ctxt max_solutions)) false crits);
 
     fun prt_result (goal, results) =
       let