--- a/src/HOL/TPTP/MaSh_Export.thy Sat Jun 28 22:13:23 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy Sun Jun 29 18:28:27 2014 +0200
@@ -46,22 +46,22 @@
()
*}
-ML {* Options.put_default @{system_option MaSh} "sml_nb" *}
+ML {* Options.put_default @{system_option MaSh} "nb" *}
ML {*
if do_it then
generate_mash_suggestions @{context} params (range, step) thys max_suggestions
- (prefix ^ "mash_sml_nb_suggestions")
+ (prefix ^ "mash_nb_suggestions")
else
()
*}
-ML {* Options.put_default @{system_option MaSh} "sml_knn" *}
+ML {* Options.put_default @{system_option MaSh} "knn" *}
ML {*
if do_it then
generate_mash_suggestions @{context} params (range, step) thys max_suggestions
- (prefix ^ "mash_sml_knn_suggestions")
+ (prefix ^ "mash_knn_suggestions")
else
()
*}