# HG changeset patch
# User blanchet
# Date 1411986612 -7200
# Node ID 9953ab32d9c24ea66729c8c8ce4a820f355c5f06
# Parent  d15707791817923407edad93b0b73e952d8d13e6
fixed wrong optimization (wrong because it may affect the sequent's conclusion)

diff -r d15707791817 -r 9953ab32d9c2 src/HOL/Tools/ATP/atp_proof_redirect.ML
--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML	Mon Sep 29 12:30:09 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML	Mon Sep 29 12:30:12 2014 +0200
@@ -131,8 +131,6 @@
   | 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 cases]
-
 fun descendants direct_graph = these o try (Atom_Graph.all_succs direct_graph) o single
 
 fun zones_of 0 _ = []
@@ -167,9 +165,8 @@
           val subseqss = map (subsequents seqs) zones
           val seqs = fold (subtract direct_sequent_eq) subseqss seqs
           val cases = map2 (fn l => fn subseqs => ([l], redirect [l] proved subseqs)) c subseqss
-          val cases' = filter_out (null o snd) cases
         in
-          s_cases cases' @ redirect (succedent_of_cases cases) proved seqs
+          Cases cases :: redirect (succedent_of_cases cases) proved seqs
         end
   in
     redirect [] axioms seqs