src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

   | MaSh_NB_Ext
   | MaSh_kNN_Ext
 
   val is_mash_enabled : unit -> bool
   val the_mash_algorithm : unit -> mash_algorithm
+  val str_of_mash_algorithm : mash_algorithm -> string
 
   val mesh_facts : ('a * 'a -> bool) -> int -> (real * (('a * real) list * 'a list)) list -> 'a list
   val nickname_of_thm : thm -> string
   val find_suggested_facts : Proof.context -> ('b * thm) list -> string list -> ('b * thm) list
   val crude_thm_ord : thm * thm -> order

     | algorithm => (warning ("Unknown MaSh algorithm: " ^ quote algorithm ^ "."); NONE))
   end
 
 val is_mash_enabled = is_some o mash_algorithm
 val the_mash_algorithm = the_default MaSh_NB_kNN o mash_algorithm
+
+fun str_of_mash_algorithm MaSh_NB = "nb"
+  | str_of_mash_algorithm MaSh_kNN = "knn"
+  | str_of_mash_algorithm MaSh_NB_kNN = "nb_knn"
+  | str_of_mash_algorithm MaSh_NB_Ext = "nb_ext"
+  | str_of_mash_algorithm MaSh_kNN_Ext = "knn_ext"
 
 fun scaled_avg [] = 0
   | scaled_avg xs = Real.ceil (100000000.0 * fold (curry (op +)) xs 0.0) div length xs
 
 fun avg [] = 0.0