# HG changeset patch
# User blanchet
# Date 1412067986 -7200
# Node ID 558459615a73ae7217106d1676dc656b6158d6e3
# Parent  289d1c39968c8ffb34986cdc4a7df89f5c6749a9
keep rules with no premises in Isar proofs from veriT

diff -r 289d1c39968c -r 558459615a73 src/HOL/Tools/SMT/verit_isar.ML
--- a/src/HOL/Tools/SMT/verit_isar.ML	Tue Sep 30 10:25:04 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_isar.ML	Tue Sep 30 11:06:26 2014 +0200
@@ -50,7 +50,7 @@
                   name0 :: normalizing_prems ctxt concl0)]
               end)
           end
-        else if rule = veriT_tmp_ite_elim_rule then
+        else if rule = veriT_tmp_ite_elim_rule orelse null prems then
           [standard_step Lemma]
         else
           [standard_step Plain]