src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
changeset 62219 dbac573b27e7
parent 61666 f1b257607981
child 62826 eb94e570c1a4
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 01 18:45:18 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 01 19:57:58 2016 +0100
@@ -173,7 +173,7 @@
               (* check if the modified step can be preplayed fast enough *)
               val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l'))
             in
-              (case preplay_isar_step ctxt timeout hopeless step'' of
+              (case preplay_isar_step ctxt [] timeout hopeless step'' of
                 meths_outcomes as (_, Played time'') :: _ =>
                 (* "l'" successfully eliminated *)
                 (decrement_step_count ();
@@ -218,7 +218,8 @@
                   val total_time = Library.foldl Time.+ (reference_time l, times0)
                   val timeout = adjust_merge_timeout preplay_timeout
                     (Time.fromReal (Time.toReal total_time / Real.fromInt n))
-                  val meths_outcomess = @{map 2} (preplay_isar_step ctxt timeout) hopelesses succs'
+                  val meths_outcomess =
+                    @{map 2} (preplay_isar_step ctxt [] timeout) hopelesses succs'
                 in
                   (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
                     NONE => steps