1.1 --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Sun Dec 15 20:31:25 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Sun Dec 15 22:03:12 2013 +0100
     1.3 @@ -132,7 +132,7 @@
     1.4    | succedent_of_case (_, infs) = succedent_of_inference (List.last infs)
     1.5  and succedent_of_cases cases = disj (map succedent_of_case cases)
     1.6  
     1.7 -fun s_cases cases = [Cases (filter_out (null o snd) cases)]
     1.8 +fun s_cases cases = [Cases cases]
     1.9  
    1.10  fun descendants direct_graph = these o try (Atom_Graph.all_succs direct_graph) o single
    1.11  
    1.12 @@ -183,7 +183,7 @@
    1.13  
    1.14  fun string_of_rich_sequent ch (id, (cs, c)) =
    1.15    (if null cs then "" else commas (map string_of_clause cs) ^ " ") ^ ch ^ " " ^ string_of_clause c ^
    1.16 -  " (* " ^ Atom.string_of id ^ "*)"
    1.17 +  " (* " ^ Atom.string_of id ^ " *)"
    1.18  
    1.19  fun string_of_case depth (c, proof) =
    1.20    indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]"

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 20:31:25 2013 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Dec 15 22:03:12 2013 +0100
     2.3 @@ -16,10 +16,9 @@
     2.4      bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
     2.5      thm
     2.6  
     2.7 -  val isar_proof_text :
     2.8 -    Proof.context -> bool option -> isar_params -> one_line_params -> string
     2.9 -  val proof_text :
    2.10 -    Proof.context -> bool option -> (unit -> isar_params) -> int -> one_line_params -> string
    2.11 +  val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string
    2.12 +  val proof_text : Proof.context -> bool option -> (unit -> isar_params) -> int ->
    2.13 +    one_line_params -> string
    2.14  end;
    2.15  
    2.16  structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
    2.17 @@ -382,7 +381,8 @@
    2.18                val l = label_of_clause c
    2.19                val t = prop_of_clause c
    2.20                val step =
    2.21 -                Prove (maybe_show outer c [], [], l, t, map isar_case cases,
    2.22 +                Prove (maybe_show outer c [], [], l, t,
    2.23 +                  map isar_case (filter_out (null o snd) cases),
    2.24                    ((the_list predecessor, []), MetisM))
    2.25              in
    2.26                isar_steps outer (SOME l) (step :: accum) infs
    2.27 @@ -445,6 +445,7 @@
    2.28              Active.sendback_markup [Markup.padding_command] isar_text
    2.29            end)
    2.30        end
    2.31 +
    2.32      val isar_proof =
    2.33        if debug then
    2.34          isar_proof_of ()