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 ^ "]"