--- a/src/HOL/Tools/Sledgehammer/MaSh/src/stats.py Fri Aug 23 15:07:32 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/stats.py Fri Aug 23 15:49:27 2013 +0200
@@ -123,6 +123,8 @@
# HACK FOR PAPER
assert len(self.aucData) == len(self.recall100Median)
nrDataPoints = len(self.aucData)
+ if nrDataPoints == 0:
+ return "No data points"
if nrDataPoints % 2 == 1:
medianAUC = sorted(self.aucData)[nrDataPoints/2 + 1]
else:
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 23 15:07:32 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 23 15:49:27 2013 +0200
@@ -635,7 +635,7 @@
add_type_pat depth t #> add_type_pats (depth - 1) t
fun add_type T =
add_type_pats type_max_depth T
- #> fold_atyps_sorts (fn (_, S) => add_classes S) T
+ #> fold_atyps_sorts (add_classes o snd) T
fun add_subtypes (T as Type (_, Ts)) = add_type T #> fold add_subtypes Ts
| add_subtypes T = add_type T