1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 22 03:29:35 2014 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 22 03:29:36 2014 +0200
1.3 @@ -289,7 +289,7 @@
1.4 val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
1.5
1.6 val _ = fold_isar_steps (fn meth =>
1.7 - K (set_preplay_outcomes_of_isar_step ctxt debug preplay_timeout preplay_data meth []))
1.8 + K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
1.9 (steps_of_isar_proof canonical_isar_proof) ()
1.10
1.11 fun str_of_preplay_outcome outcome =
1.12 @@ -316,11 +316,11 @@
1.13 val (play_outcome, isar_proof) =
1.14 canonical_isar_proof
1.15 |> tap (trace_isar_proof "Original")
1.16 - |> compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data
1.17 + |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
1.18 |> tap (trace_isar_proof "Compressed")
1.19 |> postprocess_isar_proof_remove_unreferenced_steps
1.20 (keep_fastest_method_of_isar_step (!preplay_data)
1.21 - #> minimize ? minimize_isar_step_dependencies ctxt debug preplay_data)
1.22 + #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
1.23 |> tap (trace_isar_proof "Minimized")
1.24 (* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an
1.25 unnatural semantics): *)
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu May 22 03:29:35 2014 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Thu May 22 03:29:36 2014 +0200
2.3 @@ -11,7 +11,7 @@
2.4 type isar_proof = Sledgehammer_Isar_Proof.isar_proof
2.5 type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
2.6
2.7 - val compress_isar_proof : Proof.context -> bool -> real -> Time.time ->
2.8 + val compress_isar_proof : Proof.context -> real -> Time.time ->
2.9 isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof
2.10 end;
2.11
2.12 @@ -109,7 +109,7 @@
2.13 val compress_degree = 2
2.14
2.15 (* Precondition: The proof must be labeled canonically. *)
2.16 -fun compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data proof =
2.17 +fun compress_isar_proof ctxt compress_isar preplay_timeout preplay_data proof =
2.18 if compress_isar <= 1.0 then
2.19 proof
2.20 else
2.21 @@ -172,12 +172,11 @@
2.22 (* check if the modified step can be preplayed fast enough *)
2.23 val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l'))
2.24 in
2.25 - (case preplay_isar_step ctxt debug timeout hopeless step'' of
2.26 + (case preplay_isar_step ctxt timeout hopeless step'' of
2.27 meths_outcomes as (_, Played time'') :: _ =>
2.28 (* l' successfully eliminated *)
2.29 (decrement_step_count ();
2.30 - set_preplay_outcomes_of_isar_step ctxt debug time'' preplay_data step''
2.31 - meths_outcomes;
2.32 + set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes;
2.33 map (replace_successor l' [l]) lfs';
2.34 elim_one_subproof time'' step'' subs nontriv_subs)
2.35 | _ => elim_one_subproof time step subs (sub :: nontriv_subs))
2.36 @@ -217,15 +216,14 @@
2.37 val timeouts =
2.38 map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0
2.39 val meths_outcomess =
2.40 - map3 (preplay_isar_step ctxt debug) timeouts hopelesses succs'
2.41 + map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
2.42 in
2.43 (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
2.44 NONE => steps
2.45 | SOME times =>
2.46 (* candidate successfully eliminated *)
2.47 (decrement_step_count ();
2.48 - map3 (fn time =>
2.49 - set_preplay_outcomes_of_isar_step ctxt debug time preplay_data)
2.50 + map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data)
2.51 times succs' meths_outcomess;
2.52 map (replace_successor l labels) lfs;
2.53 steps_before @ update_steps succs' steps_after))
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu May 22 03:29:35 2014 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Thu May 22 03:29:36 2014 +0200
3.3 @@ -12,8 +12,8 @@
3.4 type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
3.5
3.6 val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step
3.7 - val minimize_isar_step_dependencies : Proof.context -> bool ->
3.8 - isar_preplay_data Unsynchronized.ref -> isar_step -> isar_step
3.9 + val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
3.10 + isar_step -> isar_step
3.11 val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
3.12 isar_proof
3.13 end;
3.14 @@ -34,7 +34,7 @@
3.15
3.16 val slack = seconds 0.025
3.17
3.18 -fun minimize_isar_step_dependencies ctxt debug preplay_data
3.19 +fun minimize_isar_step_dependencies ctxt preplay_data
3.20 (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
3.21 (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
3.22 Played time =>
3.23 @@ -43,7 +43,7 @@
3.24
3.25 fun minimize_facts _ min_facts [] time = (min_facts, time)
3.26 | minimize_facts mk_step min_facts (fact :: facts) time =
3.27 - (case preplay_isar_step_for_method ctxt debug (Time.+ (time, slack)) meth
3.28 + (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth
3.29 (mk_step (min_facts @ facts)) of
3.30 Played time' => minimize_facts mk_step min_facts facts time'
3.31 | _ => minimize_facts mk_step (fact :: min_facts) facts time)
3.32 @@ -53,12 +53,11 @@
3.33
3.34 val step' = mk_step_lfs_gfs min_lfs min_gfs
3.35 in
3.36 - set_preplay_outcomes_of_isar_step ctxt debug time'' preplay_data step'
3.37 - [(meth, Played time'')];
3.38 + set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step' [(meth, Played time'')];
3.39 step'
3.40 end
3.41 | _ => step (* don't touch steps that time out or fail *))
3.42 - | minimize_isar_step_dependencies _ _ _ step = step
3.43 + | minimize_isar_step_dependencies _ _ step = step
3.44
3.45 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
3.46 let
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu May 22 03:29:35 2014 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Thu May 22 03:29:36 2014 +0200
4.3 @@ -18,11 +18,11 @@
4.4 type isar_preplay_data
4.5
4.6 val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
4.7 - val preplay_isar_step_for_method : Proof.context -> bool -> Time.time -> proof_method ->
4.8 - isar_step -> play_outcome
4.9 - val preplay_isar_step : Proof.context -> bool -> Time.time -> proof_method list -> isar_step ->
4.10 + val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
4.11 + play_outcome
4.12 + val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step ->
4.13 (proof_method * play_outcome) list
4.14 - val set_preplay_outcomes_of_isar_step : Proof.context -> bool -> Time.time ->
4.15 + val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
4.16 isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit
4.17 val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
4.18 val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method ->
4.19 @@ -101,8 +101,7 @@
4.20 end
4.21
4.22 (* may throw exceptions *)
4.23 -fun raw_preplay_step_for_method ctxt debug timeout meth
4.24 - (Prove (_, xs, _, t, subproofs, facts, _, _)) =
4.25 +fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
4.26 let
4.27 val goal =
4.28 (case xs of
4.29 @@ -129,7 +128,7 @@
4.30
4.31 fun prove () =
4.32 Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
4.33 - HEADGOAL (tac_of_proof_method ctxt debug assmsp meth))
4.34 + HEADGOAL (tac_of_proof_method ctxt assmsp meth))
4.35 handle ERROR msg => error ("Preplay error: " ^ msg)
4.36
4.37 val play_outcome = take_time timeout prove ()
4.38 @@ -138,13 +137,13 @@
4.39 play_outcome
4.40 end
4.41
4.42 -fun preplay_isar_step_for_method ctxt debug timeout meth =
4.43 - try (raw_preplay_step_for_method ctxt debug timeout meth) #> the_default Play_Failed
4.44 +fun preplay_isar_step_for_method ctxt timeout meth =
4.45 + try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed
4.46
4.47 -fun preplay_isar_step ctxt debug timeout hopeless step =
4.48 +fun preplay_isar_step ctxt timeout hopeless step =
4.49 let
4.50 fun try_method meth =
4.51 - (case preplay_isar_step_for_method ctxt debug timeout meth step of
4.52 + (case preplay_isar_step_for_method ctxt timeout meth step of
4.53 outcome as Played _ => SOME (meth, outcome)
4.54 | _ => NONE)
4.55
4.56 @@ -164,11 +163,11 @@
4.57 | add_preplay_outcomes play1 play2 =
4.58 Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
4.59
4.60 -fun set_preplay_outcomes_of_isar_step ctxt debug timeout preplay_data
4.61 +fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
4.62 (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
4.63 let
4.64 fun lazy_preplay meth =
4.65 - Lazy.lazy (fn () => preplay_isar_step_for_method ctxt debug timeout meth step)
4.66 + Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
4.67 val meths_outcomes = meths_outcomes0
4.68 |> map (apsnd Lazy.value)
4.69 |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
4.70 @@ -176,7 +175,7 @@
4.71 preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes [])
4.72 (!preplay_data)
4.73 end
4.74 - | set_preplay_outcomes_of_isar_step _ _ _ _ _ _ = ()
4.75 + | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
4.76
4.77 fun peek_at_outcome outcome =
4.78 if Lazy.is_finished outcome then Lazy.force outcome else Play_Timed_Out Time.zeroTime
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu May 22 03:29:35 2014 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Thu May 22 03:29:36 2014 +0200
5.3 @@ -34,8 +34,7 @@
5.4 (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
5.5
5.6 val string_of_proof_method : Proof.context -> string list -> proof_method -> string
5.7 - val tac_of_proof_method : Proof.context -> bool -> thm list * thm list -> proof_method -> int ->
5.8 - tactic
5.9 + val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
5.10 val string_of_play_outcome : play_outcome -> string
5.11 val play_outcome_ord : play_outcome * play_outcome -> order
5.12 val one_line_proof_text : Proof.context -> int -> one_line_params -> string
5.13 @@ -97,7 +96,7 @@
5.14 maybe_paren (space_implode " " (meth_s :: ss))
5.15 end
5.16
5.17 -fun tac_of_proof_method ctxt debug (local_facts, global_facts) meth =
5.18 +fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
5.19 Method.insert_tac local_facts THEN'
5.20 (case meth of
5.21 Metis_Method (type_enc_opt, lam_trans_opt) =>
6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu May 22 03:29:35 2014 +0200
6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu May 22 03:29:36 2014 +0200
6.3 @@ -79,7 +79,7 @@
6.4 val filter_used_facts :
6.5 bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
6.6 ((''a * stature) * 'b) list
6.7 - val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
6.8 + val play_one_line_proof : mode -> bool -> Time.time -> ((string * 'a) * thm) list ->
6.9 Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
6.10 val isar_supported_prover_of : theory -> string -> string
6.11 val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
6.12 @@ -214,15 +214,15 @@
6.13 TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
6.14 end
6.15
6.16 -fun timed_proof_method debug timeout ths meth =
6.17 - timed_apply timeout (fn ctxt => tac_of_proof_method ctxt debug ([], ths) meth)
6.18 +fun timed_proof_method timeout ths meth =
6.19 + timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
6.20
6.21 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
6.22
6.23 fun filter_used_facts keep_chained used =
6.24 filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
6.25
6.26 -fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
6.27 +fun play_one_line_proof mode verbose timeout pairs state i preferred (meths as meth :: _) =
6.28 let
6.29 val ctxt = Proof.context_of state
6.30
6.31 @@ -246,7 +246,7 @@
6.32 ()
6.33 val timer = Timer.startRealTimer ()
6.34 in
6.35 - (case timed_proof_method debug timeout ths meth state i of
6.36 + (case timed_proof_method timeout ths meth state i of
6.37 SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
6.38 | _ => play timed_out meths)
6.39 end
7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu May 22 03:29:35 2014 +0200
7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu May 22 03:29:36 2014 +0200
7.3 @@ -353,8 +353,8 @@
7.4 (used_facts,
7.5 Lazy.lazy (fn () =>
7.6 let val used_pairs = used_from |> filter_used_facts false used_facts in
7.7 - play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
7.8 - (hd meths) meths
7.9 + play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal (hd meths)
7.10 + meths
7.11 end),
7.12 fn preplay =>
7.13 let
8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu May 22 03:29:35 2014 +0200
8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Thu May 22 03:29:36 2014 +0200
8.3 @@ -51,7 +51,7 @@
8.4 open Sledgehammer_Prover_SMT
8.5 open Sledgehammer_Prover_SMT2
8.6
8.7 -fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
8.8 +fun run_proof_method mode name (params as {verbose, timeout, type_enc, lam_trans, ...})
8.9 minimize_command
8.10 ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
8.11 let
8.12 @@ -61,23 +61,22 @@
8.13 else raise Fail ("unknown proof_method: " ^ quote name)
8.14 val used_facts = facts |> map fst
8.15 in
8.16 - (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout
8.17 - facts state subgoal meth [meth] of
8.18 + (case play_one_line_proof (if mode = Minimize then Normal else mode) verbose timeout facts state
8.19 + subgoal meth [meth] of
8.20 play as (_, Played time) =>
8.21 {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
8.22 preplay = Lazy.value play,
8.23 - message =
8.24 - fn play =>
8.25 - let
8.26 - val ctxt = Proof.context_of state
8.27 - val (_, override_params) = extract_proof_method params meth
8.28 - val one_line_params =
8.29 - (play, proof_banner mode name, used_facts, minimize_command override_params name,
8.30 - subgoal, subgoal_count)
8.31 - val num_chained = length (#facts (Proof.goal state))
8.32 - in
8.33 - one_line_proof_text ctxt num_chained one_line_params
8.34 - end,
8.35 + message = fn play =>
8.36 + let
8.37 + val ctxt = Proof.context_of state
8.38 + val (_, override_params) = extract_proof_method params meth
8.39 + val one_line_params =
8.40 + (play, proof_banner mode name, used_facts, minimize_command override_params name,
8.41 + subgoal, subgoal_count)
8.42 + val num_chained = length (#facts (Proof.goal state))
8.43 + in
8.44 + one_line_proof_text ctxt num_chained one_line_params
8.45 + end,
8.46 message_tail = ""}
8.47 | play =>
8.48 let
8.49 @@ -128,10 +127,7 @@
8.50 fun n_facts names =
8.51 let val n = length names in
8.52 string_of_int n ^ " fact" ^ plural_s n ^
8.53 - (if n > 0 then
8.54 - ": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
8.55 - else
8.56 - "")
8.57 + (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "")
8.58 end
8.59
8.60 fun print silent f = if silent then () else Output.urgent_message (f ())
8.61 @@ -141,10 +137,9 @@
8.62 smt_proofs, preplay_timeout, ...} : params)
8.63 silent (prover : prover) timeout i n state goal facts =
8.64 let
8.65 - val _ =
8.66 - print silent (fn () =>
8.67 - "Testing " ^ n_facts (map fst facts) ^
8.68 - (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
8.69 + val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
8.70 + (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
8.71 +
8.72 val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
8.73 val params =
8.74 {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
8.75 @@ -230,7 +225,7 @@
8.76 (case test timeout (sup @ r0) of
8.77 result as {outcome = NONE, used_facts, ...} =>
8.78 min depth result (filter_used_facts true used_facts sup)
8.79 - (filter_used_facts true used_facts r0)
8.80 + (filter_used_facts true used_facts r0)
8.81 | _ =>
8.82 let
8.83 val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
8.84 @@ -259,8 +254,8 @@
8.85 val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
8.86 fun test timeout = test_facts params silent prover timeout i n state goal
8.87 val (chained, non_chained) = List.partition is_fact_chained facts
8.88 - (* Push chained facts to the back, so that they are less likely to be
8.89 - kicked out by the linear minimization algorithm. *)
8.90 + (* Push chained facts to the back, so that they are less likely to be kicked out by the linear
8.91 + minimization algorithm. *)
8.92 val facts = non_chained @ chained
8.93 in
8.94 (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ ".");
8.95 @@ -378,8 +373,7 @@
8.96 | NONE => result)
8.97 end
8.98
8.99 -fun get_minimizing_prover ctxt mode do_learn name params minimize_command
8.100 - problem =
8.101 +fun get_minimizing_prover ctxt mode do_learn name params minimize_command problem =
8.102 get_prover ctxt mode name params minimize_command problem
8.103 |> maybe_minimize ctxt mode do_learn name params problem
8.104
8.105 @@ -393,14 +387,14 @@
8.106 in
8.107 (case subgoal_count state of
8.108 0 => Output.urgent_message "No subgoal!"
8.109 - | n => (case provers of
8.110 - [] => error "No prover is set."
8.111 - | prover :: _ =>
8.112 - (kill_provers ();
8.113 - minimize_facts do_learn prover params false i n state goal NONE facts
8.114 - |> (fn (_, (preplay, message, message_tail)) =>
8.115 - message (Lazy.force preplay) ^ message_tail
8.116 - |> Output.urgent_message))))
8.117 + | n =>
8.118 + (case provers of
8.119 + [] => error "No prover is set."
8.120 + | prover :: _ =>
8.121 + (kill_provers ();
8.122 + minimize_facts do_learn prover params false i n state goal NONE facts
8.123 + |> (fn (_, (preplay, message, message_tail)) =>
8.124 + Output.urgent_message (message (Lazy.force preplay) ^ message_tail)))))
8.125 end
8.126
8.127 end;
9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu May 22 03:29:35 2014 +0200
9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu May 22 03:29:36 2014 +0200
9.3 @@ -212,7 +212,7 @@
9.4 do_slice timeout 1 NONE Time.zeroTime
9.5 end
9.6
9.7 -fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
9.8 +fun run_smt_solver mode name (params as {verbose, smt_proofs, preplay_timeout, ...})
9.9 minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
9.10 let
9.11 val thy = Proof.theory_of state
9.12 @@ -233,7 +233,7 @@
9.13 (case outcome of
9.14 NONE =>
9.15 (Lazy.lazy (fn () =>
9.16 - play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
9.17 + play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal
9.18 SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
9.19 fn preplay =>
9.20 let
10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 03:29:35 2014 +0200
10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 03:29:36 2014 +0200
10.3 @@ -238,7 +238,7 @@
10.4 (case outcome of
10.5 NONE =>
10.6 (Lazy.lazy (fn () =>
10.7 - play_one_line_proof mode debug verbose preplay_timeout used_named_facts state subgoal
10.8 + play_one_line_proof mode verbose preplay_timeout used_named_facts state subgoal
10.9 SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
10.10 fn preplay =>
10.11 let