src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py

         self.accessibleDict = {}
         self.expandedAccessibles = {}
         self.changed = True
 
     """
-    Init functions. Side Effect: nameIdDict, idNameDict, featureIdDict get filled!
+    Init functions. Side Effect: nameIdDict, idNameDict, featureIdDict, articleDict get filled!
     """
     def init_featureDict(self,featureFile):
         self.featureDict,self.maxNameId,self.maxFeatureId = create_feature_dict(self.nameIdDict,self.idNameDict,self.maxNameId,self.featureIdDict,\
                                                                                 self.maxFeatureId,featureFile)
     def init_dependenciesDict(self,depFile):

             if not self.expandedAccessibles.has_key(accId):
                 accIdAcc = self.accessibleDict[accId]
                 self.expandedAccessibles[accId] = self.expand_accessibles(accIdAcc)
                 self.changed = True
         accessibles = self.expand_accessibles(unExpAcc)
-#        # Feature Ids
-#        featureNames = [f.strip() for f in line[1].split()]
-#        for fn in featureNames:
-#            self.add_feature(fn)
-#        features = [self.featureIdDict[fn] for fn in featureNames]
         features = self.get_features(line)
+
         return name,features,accessibles
 
     def save(self,fileName):
         if self.changed:
             dictsStream = open(fileName, 'wb')