don't learn theories -- this option is very slow and not very helpful

--- 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 " ^