# HG changeset patch
# User blanchet
# Date 1422882093 -3600
# Node ID 1b3385de296de0bff9bdc67315110b4a13e7c161
# Parent  90f5bab83c3184f2792796a340a10399aa62c13c
less confusing constant

diff -r 90f5bab83c31 -r 1b3385de296d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 02 14:01:33 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 02 14:01:33 2015 +0100
@@ -367,7 +367,7 @@
     ret (Integer.max 0 (num_facts - max_suggs)) []
   end
 
-val initial_number_of_nearest_neighbors = 1
+val initial_k = 0
 
 fun k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs visible_facts goal_feats =
   let
@@ -425,7 +425,7 @@
         end
 
     fun while1 () =
-      if !k = initial_number_of_nearest_neighbors then () else (do_k (!k); k := !k + 1; while1 ())
+      if !k = initial_k + 1 then () else (do_k (!k); k := !k + 1; while1 ())
       handle EXIT () => ()
 
     fun while2 () =
@@ -479,7 +479,7 @@
   end
 
 fun k_nearest_neighbors_ext max_suggs =
-  external_tool ("newknn/knn" ^ " " ^ string_of_int initial_number_of_nearest_neighbors) max_suggs
+  external_tool ("newknn/knn" ^ " " ^ string_of_int initial_k) max_suggs
 fun naive_bayes_ext max_suggs = external_tool "predict/nbayes" max_suggs
 
 fun query_external ctxt algorithm max_suggs learns goal_feats =