# HG changeset patch
# User blanchet
# Date 1356619587 -3600
# Node ID f104b10af6e7f04e5589e59926e913667e98dba5
# Parent  512dfe5e077fc9e138178ba1a10f5fdd275488c7
enable theory learning in MaSh

diff -r 512dfe5e077f -r f104b10af6e7 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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