# 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