--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 20:31:25 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Dec 15 22:03:12 2013 +0100
@@ -16,10 +16,9 @@
bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
thm
- val isar_proof_text :
- Proof.context -> bool option -> isar_params -> one_line_params -> string
- val proof_text :
- Proof.context -> bool option -> (unit -> isar_params) -> int -> one_line_params -> string
+ val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string
+ val proof_text : Proof.context -> bool option -> (unit -> isar_params) -> int ->
+ one_line_params -> string
end;
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
@@ -382,7 +381,8 @@
val l = label_of_clause c
val t = prop_of_clause c
val step =
- Prove (maybe_show outer c [], [], l, t, map isar_case cases,
+ Prove (maybe_show outer c [], [], l, t,
+ map isar_case (filter_out (null o snd) cases),
((the_list predecessor, []), MetisM))
in
isar_steps outer (SOME l) (step :: accum) infs
@@ -445,6 +445,7 @@
Active.sendback_markup [Markup.padding_command] isar_text
end)
end
+
val isar_proof =
if debug then
isar_proof_of ()