src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 50869 67bb94a6f780
parent 50861 fa4253914e98
child 50874 2eae85887282
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jan 13 22:00:45 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jan 13 22:17:00 2013 +0100
@@ -150,7 +150,7 @@
     val core =
       "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
       " --numberOfPredictions " ^ string_of_int max_suggs ^
-      " --learnTheories --NBSinePrior" ^
+      " --NBSinePrior" (* --learnTheories *) ^
       (if save then " --saveModel" else "")
     val command =
       "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^