# HG changeset patch
# User blanchet
# Date 1405439394 -7200
# Node ID 8200e1eb367f746a63fc09cfc201452488541cbc
# Parent  bc957769b584a349a45c4afb6b72f90dac77ef23
made SML/NJ happier

diff -r bc957769b584 -r 8200e1eb367f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 15 11:13:43 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 15 17:49:54 2014 +0200
@@ -477,9 +477,9 @@
      forkexec max_suggs)
   end
 
-val k_nearest_neighbors_ext =
-  external_tool ("newknn/knn" ^ " " ^ string_of_int initial_number_of_nearest_neighbors)
-val naive_bayes_ext = external_tool "predict/nbayes"
+fun k_nearest_neighbors_ext max_suggs =
+  external_tool ("newknn/knn" ^ " " ^ string_of_int initial_number_of_nearest_neighbors) max_suggs
+fun naive_bayes_ext max_suggs = external_tool "predict/nbayes" max_suggs
 
 fun query_external ctxt algorithm max_suggs learns goal_feats =
   (trace_msg ctxt (fn () => "MaSh query external " ^ commas (map fst goal_feats));