--- a/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py Mon Dec 09 04:03:30 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/dictionaries.py Mon Dec 09 04:03:30 2013 +0100
@@ -105,10 +105,7 @@
self.changed = True
fId = self.featureIdDict[f]
fIds.append(fId)
- if len(fIds) == 1:
- return fIds[0]
- else:
- return fIds
+ return fIds
def get_features(self,line):
featureNames = [f.strip() for f in line[1].split()]
@@ -119,8 +116,8 @@
if len(tmp) == 2:
fn = tmp[0]
weight = float(tmp[1])
- fId = self.add_feature(tmp[0])
- features[fId] = weight
+ fIds = self.add_feature(tmp[0])
+ features[fIds[0]] = (weight,fIds[1:])
#features[fId] = 1.0 ###
return features