1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 15 00:21:32 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 15 00:21:32 2014 +0200
     1.3 @@ -243,7 +243,8 @@
     1.4                  0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
     1.5                    |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor))
     1.6              val _ = spying spy (fn () => (state, i, "All",
     1.7 -              "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
     1.8 +              "Filtering " ^ string_of_int (length all_facts) ^ " facts (MaSh algorithm: " ^
     1.9 +              str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
    1.10            in
    1.11              all_facts
    1.12              |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 15 00:21:32 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Jul 15 00:21:32 2014 +0200
     2.3 @@ -42,6 +42,7 @@
     2.4  
     2.5    val is_mash_enabled : unit -> bool
     2.6    val the_mash_algorithm : unit -> mash_algorithm
     2.7 +  val str_of_mash_algorithm : mash_algorithm -> string
     2.8  
     2.9    val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
    2.10    val nickname_of_thm : thm -> string
    2.11 @@ -154,6 +155,12 @@
    2.12  val is_mash_enabled = is_some o mash_algorithm
    2.13  val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm
    2.14  
    2.15 +fun str_of_mash_algorithm MaSh_NB = "nb"
    2.16 +  | str_of_mash_algorithm MaSh_kNN = "knn"
    2.17 +  | str_of_mash_algorithm MaSh_NB_kNN = "nb_knn"
    2.18 +  | str_of_mash_algorithm MaSh_NB_Ext = "nb_ext"
    2.19 +  | str_of_mash_algorithm MaSh_kNN_Ext = "knn_ext"
    2.20 +
    2.21  fun scaled_avg [] = 0
    2.22    | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
    2.23