# HG changeset patch
# User blanchet
# Date 1412264378 -7200
# Node ID 6cf55e935a9d56b903f7fc5c7515033e51588d83
# Parent  1fc93ea5136b912e07fbb2aa785fb21ab32a105f
avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition

diff -r 1fc93ea5136b -r 6cf55e935a9d src/HOL/Tools/SMT/verit_isar.ML
--- a/src/HOL/Tools/SMT/verit_isar.ML	Thu Oct 02 15:24:51 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_isar.ML	Thu Oct 02 17:39:38 2014 +0200
@@ -50,10 +50,8 @@
                   name0 :: normalizing_prems ctxt concl0)]
               end)
           end
-        else if rule = veriT_tmp_ite_elim_rule orelse null prems then
-          [standard_step Lemma]
         else
-          [standard_step Plain]
+          [standard_step (if null prems then Lemma else Plain)]
       end
   in
     maps steps_of