avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition

--- 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