--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu Aug 28 16:58:27 2014 +0200
@@ -17,6 +17,7 @@
type isar_preplay_data
+ val peek_at_outcome : play_outcome Lazy.lazy -> play_outcome
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
play_outcome
@@ -41,6 +42,9 @@
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
+fun peek_at_outcome outcome =
+ if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
+
fun par_list_map_filter_with_timeout _ _ _ _ [] = []
| par_list_map_filter_with_timeout get_time min_timeout timeout0 f xs =
let
@@ -200,9 +204,6 @@
end
| set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
-fun peek_at_outcome outcome =
- if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
-
fun get_best_method_outcome force =
tap (List.app (K () o Lazy.future Future.default_params o snd)) (* could be parallelized *)
#> map (apsnd force)