# HG changeset patch
# User blanchet
# Date 1405157482 -7200
# Node ID 2b561e7a0512ec79c3cf7602b921f049c855e242
# Parent  2126b355f0ca6f7dee713cc8abed74fe0ea37786
tuning

diff -r 2126b355f0ca -r 2b561e7a0512 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jul 12 11:31:22 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jul 12 11:31:22 2014 +0200
@@ -367,7 +367,7 @@
     ret (Integer.max 0 (num_facts - max_suggs)) []
   end
 
-val number_of_nearest_neighbors = 1 (* FUDGE *)
+val initial_number_of_nearest_neighbors = 1
 
 fun k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs visible_facts goal_feats =
   let
@@ -424,7 +424,7 @@
         end
 
     fun while1 () =
-      if !k = number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ())
+      if !k = initial_number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ())
       handle EXIT () => ()
 
     fun while2 () =
@@ -478,7 +478,7 @@
   end
 
 val k_nearest_neighbors_ext =
-  external_tool ("newknn/knn" ^ " " ^ string_of_int number_of_nearest_neighbors)
+  external_tool ("newknn/knn" ^ " " ^ string_of_int initial_number_of_nearest_neighbors)
 val naive_bayes_ext = external_tool "predict/nbayes"
 
 fun query_external ctxt algorithm max_suggs learns goal_feats =