--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Tue Apr 23 16:30:29 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Tue Apr 23 16:30:30 2013 +0200
@@ -9,7 +9,7 @@
sig
type isar_proof = Sledgehammer_Proof.isar_proof
type preplay_time = Sledgehammer_Preplay.preplay_time
- val compress_proof :
+ val compress_and_preplay_proof :
bool -> Proof.context -> string -> string -> bool -> Time.time option
-> real -> isar_proof -> isar_proof * (bool * preplay_time)
end
@@ -46,8 +46,8 @@
fun add_list tab xs = fold (Inttab.insert_list (op =)) xs tab
(* Main function for compresing proofs *)
-fun compress_proof debug ctxt type_enc lam_trans preplay preplay_timeout
- isar_compress proof =
+fun compress_and_preplay_proof debug ctxt type_enc lam_trans preplay
+ preplay_timeout isar_compress proof =
let
(* 60 seconds seems like a good interpreation of "no timeout" *)
val preplay_timeout = preplay_timeout |> the_default (seconds 60.0)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Apr 23 16:30:29 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Apr 23 16:30:30 2013 +0200
@@ -445,7 +445,7 @@
else if nr=1 orelse member (op=) qs Then
then of_thus_hence qs
else of_show_have qs
- fun add_term term (s, ctxt)=
+ fun add_term term (s, ctxt) =
(s ^ (annotate_types ctxt term
|> with_vanilla_print_mode (Syntax.string_of_term ctxt)
|> simplify_spaces
@@ -780,7 +780,7 @@
do_proof true params assms infs
end
- val cleanup_labels_in_proof =
+ val clean_up_labels_in_proof =
chain_direct_proof
#> kill_useless_labels_in_proof
#> relabel_proof
@@ -791,10 +791,10 @@
|> (if not preplay andalso isar_compress <= 1.0 then
rpair (false, (true, seconds 0.0))
else
- compress_proof debug ctxt type_enc lam_trans preplay
+ compress_and_preplay_proof debug ctxt type_enc lam_trans preplay
preplay_timeout
(if isar_proofs = SOME true then isar_compress else 1000.0))
- |>> cleanup_labels_in_proof
+ |>> clean_up_labels_in_proof
val isar_text =
string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
isar_proof
@@ -820,8 +820,8 @@
else
[])
in
- "\n\nStructured proof "
- ^ (commas msg |> not (null msg) ? enclose "(" ")")
+ "\n\nStructured proof"
+ ^ (commas msg |> not (null msg) ? enclose " (" ")")
^ ":\n" ^ Active.sendback_markup isar_text
end
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Apr 23 16:30:29 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Apr 23 16:30:30 2013 +0200
@@ -276,7 +276,7 @@
if null smts then accum else launch_provers state "SMT solver" NONE smts
val launch_full_atps = launch_atps "ATP" NONE full_atps
val launch_ueq_atps =
- launch_atps "Unit equational provers" (SOME is_unit_equality) ueq_atps
+ launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps
fun launch_atps_and_smt_solvers () =
[launch_full_atps, launch_smts, launch_ueq_atps]
|> Par_List.map (fn f => ignore (f (unknownN, state)))