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

--- a/src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py	Wed Dec 26 11:06:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/predefined.py	Thu Dec 27 10:01:40 2012 +0100
@@ -37,8 +37,7 @@
             line = line[1].split()
             preds = [dicts.get_name_id(x.strip())for x in line]
             self.predictions[predId] = preds
-        IS.close()
-        return dicts
+        IS.close()        
 
     def update(self,dataPoint,features,dependencies):
         """