# HG changeset patch
# User blanchet
# Date 1358111820 -3600
# Node ID 67bb94a6f7808a5a7824aa17ae0f2b532eadcc97
# Parent  4b30d461b3a6ff955981735b9538461a026c0ad8
don't learn theories -- this option is very slow and not very helpful

diff -r 4b30d461b3a6 -r 67bb94a6f780 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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 " ^