--- 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)