correct inlining in veriT's subproofs.
authorfleury
Tue Sep 30 14:01:33 2014 +0200 (2014-09-30)
changeset 58493308f3c7dfb67
parent 58492 e3ee0cf5cf93
child 58494 ed380b9594b5
correct inlining in veriT's subproofs.
src/HOL/Tools/SMT/verit_proof.ML
     1.1 --- a/src/HOL/Tools/SMT/verit_proof.ML	Tue Sep 30 12:47:15 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/verit_proof.ML	Tue Sep 30 14:01:33 2014 +0200
     1.3 @@ -113,7 +113,6 @@
     1.4    else
     1.5      (node, cx)
     1.6  
     1.7 -(*FIXME: using a reference would be better to know the numbers of the steps to add*)
     1.8  fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds),
     1.9      cx)) =
    1.10    let
    1.11 @@ -121,13 +120,8 @@
    1.12        concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop}
    1.13      fun inline_assumption assumption assumption_id
    1.14          (node as VeriT_Node {id, rule, prems, concl, bounds}) =
    1.15 -      if List.find (curry (op =) assumption_id) prems <> NONE then
    1.16 -        let val prems' = filter_out (curry (op =) assumption_id) prems in
    1.17 -          mk_node id rule (filter_out (curry (op =) assumption_id) prems')
    1.18 -            (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
    1.19 -        end
    1.20 -      else
    1.21 -        node
    1.22 +      mk_node id rule (filter_out (curry (op =) assumption_id) prems)
    1.23 +        (@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds
    1.24      fun find_input_steps_and_inline [] last_step = ([], last_step)
    1.25        | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps)
    1.26            last_step =