# HG changeset patch
# User blanchet
# Date 1391418858 -3600
# Node ID fccd756ed4bbe008938890724e20d1e6365c6a31
# Parent  aae87746f41215c6398965f7a5a664ea0431f42e
crucial fix: use right version of the step

diff -r aae87746f412 -r fccd756ed4bb src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -248,7 +248,7 @@
             in
               decrement_step_count (); (* candidate successfully eliminated *)
               map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data) times
-                succs succ_meths_outcomess;
+                succs' succ_meths_outcomess;
               map (replace_successor l labels) lfs;
               (* removing the step would mess up the indices; replace with dummy step instead *)
               steps1 @ dummy_isar_step :: steps2