diff -r 9df2f825422b -r b958a94cf811 src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py	Wed Dec 26 11:06:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py	Thu Dec 27 10:01:40 2012 +0100
@@ -35,7 +35,7 @@
         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,\
@@ -175,12 +175,8 @@
                 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):