diff -r e98996c2a32c -r 68f8bd1641da src/HOL/Tools/Sledgehammer/MaSh/src/readData.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/readData.py	Thu Nov 14 15:40:06 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/readData.py	Thu Nov 14 15:57:48 2013 +0100
@@ -29,7 +29,10 @@
         nameId = nameIdDict[name]
         dependenciesIds = [nameIdDict[f.strip()] for f in line[1].split()]
         # Store results, add p proves p
-        dependenciesDict[nameId] = [nameId] + dependenciesIds
+        if nameId == 0:
+            dependenciesDict[nameId] = dependenciesIds
+        else:
+            dependenciesDict[nameId] = [nameId] + dependenciesIds
     IS.close()
     return dependenciesDict