Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
crucial fix: use right version of the step
authorblanchet
Mon, 03 Feb 2014 10:14:18 +0100
changeset 55270 fccd756ed4bb
parent 55269 aae87746f412
child 55271 e78476a99c70
crucial fix: use right version of the step
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle