# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID 670cbec816b982df708f28b1b1b9dacd2c3fb0b7
# Parent  ce40cee07fbc5909a7ec25fcdf5859874938a650
restored a bit of laziness

diff -r ce40cee07fbc -r 670cbec816b9 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -176,7 +176,7 @@
         (if outcome = SOME ATP_Proof.TimedOut then timeoutN
          else if is_some outcome then noneN
          else someN,
-         fn () => message (play_one_line_proof mode preplay_timeout used_facts state subgoal
+         fn () => message (fn () => play_one_line_proof mode preplay_timeout used_facts state subgoal
            preferred_methss)))
 
     fun go () =
diff -r ce40cee07fbc -r 670cbec816b9 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -58,7 +58,7 @@
      used_from : fact list,
      preferred_methss : proof_method * proof_method list list,
      run_time : Time.time,
-     message : (string * stature) list * (proof_method * play_outcome) -> string}
+     message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
 
   type prover = params -> prover_problem -> prover_result
 
@@ -149,7 +149,7 @@
    used_from : fact list,
    preferred_methss : proof_method * proof_method list list,
    run_time : Time.time,
-   message : (string * stature) list * (proof_method * play_outcome) -> string}
+   message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string}
 
 type prover = params -> prover_problem -> prover_result
 
diff -r ce40cee07fbc -r 670cbec816b9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -385,7 +385,7 @@
                      minimize, atp_proof, goal)
                   end
 
-                val one_line_params = (preplay, proof_banner mode name, subgoal, subgoal_count)
+                val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
                 proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
diff -r ce40cee07fbc -r 670cbec816b9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -23,7 +23,7 @@
   val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
     Proof.state -> thm -> ((string * stature) * thm list) list ->
     ((string * stature) * thm list) list option
-    * (((string * stature) list * (proof_method * play_outcome)) -> string)
+    * ((unit -> (string * stature) list * (proof_method * play_outcome)) -> string)
   val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
 end;
 
@@ -209,10 +209,10 @@
          val (min_facts, {message, ...}) = min test (new_timeout timeout run_time) result facts
        in
          print silent (fn () => cat_lines
-             ["Minimized to " ^ n_facts (map fst min_facts)] ^
-              (case min_facts |> filter is_fact_chained |> length of
-                 0 => ""
-               | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
+           ["Minimized to " ^ n_facts (map fst min_facts)] ^
+            (case min_facts |> filter is_fact_chained |> length of
+              0 => ""
+            | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
          (if learn then do_learn (maps snd min_facts) else ());
          (SOME min_facts, message)
        end
diff -r ce40cee07fbc -r 670cbec816b9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -208,7 +208,7 @@
                  (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (),
                   goal)
 
-               val one_line_params = (preplay, proof_banner mode name, subgoal, subgoal_count)
+               val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
                val num_chained = length (#facts (Proof.goal state))
              in
                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained