removed redundant code line
authorblanchet
Wed, 19 Nov 2014 10:31:15 +0100
changeset 59013 f319054e8dff
parent 59012 f4e9bd04e1d5
child 59014 cc5e34575354
removed redundant code line
src/HOL/Tools/SMT/z3_isar.ML
--- a/src/HOL/Tools/SMT/z3_isar.ML	Tue Nov 18 20:56:34 2014 +0100
+++ b/src/HOL/Tools/SMT/z3_isar.ML	Wed Nov 19 10:31:15 2014 +0100
@@ -56,7 +56,6 @@
           let
             val add_hyps = filter_out (null o inter (op =) deps o snd) hyps
             val t' = add_z3_hypotheses (map fst add_hyps) t
-            val deps' = subtract (op =) hyp_names deps
             val hyps' = fold (AList.update (op =) o apsnd (insert (op =) name)) add_hyps hyps
           in
             (name, role, t', rule, deps') :: inline_z3_hypotheses hyp_names hyps' lines