# HG changeset patch
# User blanchet
# Date 1377265767 -7200
# Node ID f79f4693868b5a8307991354458b5bad79521dfc
# Parent  2c585fdbe197d5d7d3678d579d24e55d3940a725
minor MaSh fix

diff -r 2c585fdbe197 -r f79f4693868b src/HOL/Tools/Sledgehammer/MaSh/src/stats.py
--- 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:
diff -r 2c585fdbe197 -r f79f4693868b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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