# HG changeset patch
# User fleury
# Date 1412078493 -7200
# Node ID 308f3c7dfb67ef651d5764045805ee65fb74c033
# Parent  e3ee0cf5cf9377d1781f5afef08d009145167392
correct inlining in veriT's subproofs.

diff -r e3ee0cf5cf93 -r 308f3c7dfb67 src/HOL/Tools/SMT/verit_proof.ML
--- a/src/HOL/Tools/SMT/verit_proof.ML	Tue Sep 30 12:47:15 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_proof.ML	Tue Sep 30 14:01:33 2014 +0200
@@ -113,7 +113,6 @@
   else
     (node, cx)
 
-(*FIXME: using a reference would be better to know the numbers of the steps to add*)
 fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds),
     cx)) =
   let
@@ -121,13 +120,8 @@
       concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
     fun inline_assumption assumption assumption_id
         (node as VeriT_Node {id, rule, prems, concl, bounds}) =
-      if List.find (curry (op =) assumption_id) prems <> NONE then
-        let val prems' = filter_out (curry (op =) assumption_id) prems in
-          mk_node id rule (filter_out (curry (op =) assumption_id) prems')
-            (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
-        end
-      else
-        node
+      mk_node id rule (filter_out (curry (op =) assumption_id) prems)
+        (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
     fun find_input_steps_and_inline [] last_step = ([], last_step)
       | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)
           last_step =