--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 27 12:43:41 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Dec 27 15:46:27 2012 +0100
@@ -139,6 +139,7 @@
val core =
"--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
" --numberOfPredictions " ^ string_of_int max_suggs ^
+ " --learnTheories" ^
(if save then " --saveModel" else "")
val command =
"\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet --outputDir " ^
@@ -296,7 +297,7 @@
local
-val version = "*** MaSh version 20121217a ***"
+val version = "*** MaSh version 20121227a ***"
exception Too_New of unit