# 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):