# HG changeset patch
# User blanchet
# Date 1401741526 -7200
# Node ID 5ed907407041b7bf2a5a7a1996b4a164f2e6c113
# Parent  6254c51cd2104295ff7996166511b9f446ee3c8a
avoid division by 0

diff -r 6254c51cd210 -r 5ed907407041 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Jun 02 19:21:41 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Jun 02 22:38:46 2014 +0200
@@ -241,8 +241,12 @@
                   ~1 => steps
                 | i =>
                   let val successors = get_successors l in
-                    if length successors > compress_degree then steps
-                    else compression_loop candidates' (try_eliminate i l successors steps)
+                    if length successors > compress_degree then
+                      steps
+                    else
+                      steps
+                      |> not (null successors) ? try_eliminate i l successors
+                      |> compression_loop candidates'
                   end))
 
           fun add_cand (Prove (_, _, l, t, _, _, _, _)) = cons (l, size_of_term t)