# HG changeset patch
# User blanchet
# Date 1377153747 -7200
# Node ID f08f66b55cb5d711680c3dfd25958a2043a9eff1
# Parent  4f8e156d2f1917597046f4b8d8b78acfc8543d50
minor tweaks to MaSh tool

diff -r 4f8e156d2f19 -r f08f66b55cb5 src/HOL/Tools/Sledgehammer/MaSh/src/server.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Thu Aug 22 08:42:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/server.py	Thu Aug 22 08:42:27 2013 +0200
@@ -108,8 +108,7 @@
         # Output        
         predictionNames = [str(self.server.dicts.idNameDict[p]) for p in self.server.predictions[:numberOfPredictions]]
         predictionValues = [str(x) for x in predictionValues[:numberOfPredictions]]
-        predictionsStringList = ['%s=%s' % (predictionNames[i],predictionValues[i]) for i in range(len(predictionNames))]
-        predictionsString = string.join(predictionsStringList,' ')
+        predictionsString = string.join(predictionNames,' ')
         outString = '%s: %s' % (name,predictionsString)
         self.request.sendall(outString)
     
@@ -172,4 +171,4 @@
 
     
     
-    
\ No newline at end of file
+    
diff -r 4f8e156d2f19 -r f08f66b55cb5 src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py	Thu Aug 22 08:42:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py	Thu Aug 22 08:42:27 2013 +0200
@@ -95,7 +95,7 @@
         For each accessible, predicts the probability of it being useful given the features.
         Returns a ranking of the accessibles.
         """
-        tau = 0.01 # Jasmin, change value here
+        tau = 0.05 # Jasmin, change value here
         predictions = []
         for a in accessibles:
             posA = self.counts[a][0]