--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Aug 16 23:11:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sat Aug 17 11:34:50 2013 +0200
@@ -25,9 +25,9 @@
Proof.context -> (string * stature) list vector -> 'a proof ->
string list option
val isar_proof_text :
- Proof.context -> bool -> bool option -> isar_params -> one_line_params -> string
+ Proof.context -> Properties.T -> bool option -> isar_params -> one_line_params -> string
val proof_text :
- Proof.context -> bool -> bool option -> isar_params -> int -> one_line_params
+ Proof.context -> Properties.T -> bool option -> isar_params -> int -> one_line_params
-> string
end;
@@ -412,7 +412,7 @@
* string Symtab.table * (string * stature) list vector
* (string * term) list * int Symtab.table * string proof * thm
-fun isar_proof_text ctxt auto isar_proofs
+fun isar_proof_text ctxt sendback_props isar_proofs
(debug, verbose, preplay_timeout, preplay_trace, isar_compress,
isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool,
fact_names, lifted, sym_tab, atp_proof, goal)
@@ -425,7 +425,7 @@
|> (fn fixes =>
ctxt |> Variable.set_body false
|> Proof_Context.add_fixes fixes)
- val one_line_proof = one_line_proof_text auto 0 one_line_params
+ val one_line_proof = one_line_proof_text sendback_props 0 one_line_params
val type_enc =
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
else partial_typesN
@@ -625,7 +625,7 @@
"\n\nStructured proof"
^ (commas msg |> not (null msg) ? enclose " (" ")")
^ ":\n" ^
- Active.sendback_markup (if auto then [Markup.padding_command] else []) isar_text
+ Active.sendback_markup sendback_props isar_text
end
end
val isar_proof =
@@ -645,12 +645,12 @@
| Trust_Playable _ => true
| Failed_to_Play _ => true
-fun proof_text ctxt auto isar_proofs isar_params num_chained
+fun proof_text ctxt sendback_props isar_proofs isar_params num_chained
(one_line_params as (preplay, _, _, _, _, _)) =
(if isar_proofs = SOME true orelse
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
- isar_proof_text ctxt auto isar_proofs isar_params
+ isar_proof_text ctxt sendback_props isar_proofs isar_params
else
- one_line_proof_text auto num_chained) one_line_params
+ one_line_proof_text sendback_props num_chained) one_line_params
end;