src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

     val cmd_file = temp_dir ^ "/mash_commands" ^ serial
     val cmd_path = Path.explode cmd_file
     val core =
       "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
       " --numberOfPredictions " ^ string_of_int max_suggs ^
-      " --NBSinePrior" (* --learnTheories *) ^
-      (if save then " --saveModel" else "")
+      (* " --learnTheories" ^ *) (if save then " --saveModel" else "")
     val command =
       "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^
       File.shell_path (mash_model_dir ()) ^ " --log " ^ log_file ^ " " ^ core ^
       " >& " ^ err_file
     fun run_on () =