author fleury Tue, 30 Sep 2014 14:01:33 +0200 changeset 58493 308f3c7dfb67 parent 58492 e3ee0cf5cf93 child 58494 ed380b9594b5
correct inlining in veriT's subproofs.
```--- 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 =```