# HG changeset patch
# User wenzelm
# Date 1358112616 -3600
# Node ID 3afe082ff9cd9ae7115fd4307f8b4cc0dbd2ad4a
# Parent  67bb94a6f7808a5a7824aa17ae0f2b532eadcc97# Parent  a9f07af30d6433101b6a608e239ce41a708ce815
merged

diff -r a9f07af30d64 -r 3afe082ff9cd src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jan 13 22:09:24 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Jan 13 22:30:16 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 " ^