# HG changeset patch
# User blanchet
# Date 1387141392 -3600
# Node ID a1ac3eaa0d111bbfc3c2799a8977fd839c3391ca
# Parent  b632390b5966d1c83df6a22cfceaedf66056478f
generate proper succedent for cases with trivial branches

diff -r b632390b5966 -r a1ac3eaa0d11 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Sun Dec 15 20:31:25 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Sun Dec 15 22:03:12 2013 +0100
@@ -132,7 +132,7 @@
   | succedent_of_case (_, infs) = succedent_of_inference (List.last infs)
 and succedent_of_cases cases = disj (map succedent_of_case cases)
 
-fun s_cases cases = [Cases (filter_out (null o snd) cases)]
+fun s_cases cases = [Cases cases]
 
 fun descendants direct_graph = these o try (Atom_Graph.all_succs direct_graph) o single
 
@@ -183,7 +183,7 @@
 
 fun string_of_rich_sequent ch (id, (cs, c)) =
   (if null cs then "" else commas (map string_of_clause cs) ^ " ") ^ ch ^ " " ^ string_of_clause c ^
-  " (* " ^ Atom.string_of id ^ "*)"
+  " (* " ^ Atom.string_of id ^ " *)"
 
 fun string_of_case depth (c, proof) =
   indent (depth + 1) ^ "[" ^ string_of_clause c ^ "]"
diff -r b632390b5966 -r a1ac3eaa0d11 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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 ()