src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

   val auto_minimize_max_time : real Config.T
   val minimize_facts :
     (string -> thm list -> unit) -> string -> params -> bool -> int -> int
     -> Proof.state -> ((string * stature) * thm list) list
     -> ((string * stature) * thm list) list option
-       * ((unit -> play) * (play -> string) * string)
+       * (play Lazy.lazy * (play -> string) * string)
   val get_minimizing_isar_prover :
     Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover
   val run_minimize :
     params -> (string -> thm list -> unit) -> int
     -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit

                 (timeout |> the_default (seconds 60.0)) div 1000) ^
             "\").", ""))
      | {preplay, message, ...} =>
        (NONE, (preplay, prefix "Prover error: " o message, "")))
     handle ERROR msg =>
-           (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
+           (NONE, (Lazy.value (Failed_to_Play plain_metis),
+            fn _ => "Error: " ^ msg, ""))
   end
 
 fun adjust_reconstructor_params override_params
         ({debug, verbose, overlord, blocking, provers, type_enc, strict,
          lam_trans, uncurried_aliases, learn, fact_filter, max_facts,

               fun prover_fast_enough () = can_min_fast_enough run_time
             in
               if isar_proofs then
                 ((prover_fast_enough (), (name, params)), preplay)
               else
-                let val preplay = preplay () in
-                  (case preplay of
-                     Played (reconstr, timeout) =>
-                     if can_min_fast_enough timeout then
-                       (true, extract_reconstructor params reconstr
-                              ||> (fn override_params =>
-                                      adjust_reconstructor_params
-                                          override_params params))
-                     else
-                       (prover_fast_enough (), (name, params))
-                   | _ => (prover_fast_enough (), (name, params)),
-                   K preplay)
-                end
+                (case Lazy.force preplay of
+                   Played (reconstr, timeout) =>
+                   if can_min_fast_enough timeout then
+                     (true, extract_reconstructor params reconstr
+                            ||> (fn override_params =>
+                                    adjust_reconstructor_params
+                                        override_params params))
+                   else
+                     (prover_fast_enough (), (name, params))
+                 | _ => (prover_fast_enough (), (name, params)),
+                 preplay)
             end
         else
           ((false, (name, params)), preplay)
       val minimize = minimize |> the_default perhaps_minimize
       val (used_facts, (preplay, message, _)) =

              [] => error "No prover is set."
            | prover :: _ =>
              (kill_provers ();
               minimize_facts do_learn prover params false i n state facts
               |> (fn (_, (preplay, message, message_tail)) =>
-                     message (preplay ()) ^ message_tail
+                     message (Lazy.force preplay) ^ message_tail
                      |> Output.urgent_message))
   end
 
 end;