# HG changeset patch
# User blanchet
# Date 1382095809 -7200
# Node ID 70456a8f5e6e3a75c1f9719d84dad59985e8104f
# Parent  c8cc5ab4a863ca9902f0f305cb378ca102e7eb58
repair invariant in MaSh when learning new proofs

diff -r c8cc5ab4a863 -r 70456a8f5e6e src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py	Fri Oct 18 10:43:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/sparseNaiveBayes.py	Fri Oct 18 13:30:09 2013 +0200
@@ -78,6 +78,8 @@
             self.counts[dep][0] -= 1
             for f,_w in features.items():
                 self.counts[dep][1][f] -= 1
+                if self.counts[dep][1][f] == 0:
+                    del self.counts[dep][1][f]
 
 
     def overwrite(self,problemId,newDependencies,dicts):