diff -r e913a87bd5d2 -r cac309e2b1f7 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Aug 01 20:08:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Fri Aug 01 20:15:41 2014 +0200
@@ -192,8 +192,9 @@
 
       fun compress_top_level steps =
         let
-          fun cand_key (l, t_size) = (length (get_successors l), t_size)
-          val cand_ord = prod_ord int_ord (int_ord o swap) o pairself cand_key
+          val cand_key = apfst (length o get_successors)
+          val cand_ord =
+            prod_ord int_ord (prod_ord (int_ord o swap) (int_ord o swap)) o pairself cand_key
 
           fun pop_next_candidate [] = (NONE, [])
             | pop_next_candidate (cands as (cand :: cands')) =
@@ -248,7 +249,7 @@
                       |> compression_loop candidates'
                   end))
 
-          fun add_cand (Prove (_, _, l, t, _, _, _, _)) = cons (l, size_of_term t)
+          fun add_cand (Prove (_, xs, l, t, _, _, _, _)) = cons (l, (length xs, size_of_term t))
             | add_cand _ = I
 
           (* the very last step is not a candidate *)