# HG changeset patch
# User blanchet
# Date 1416389475 -3600
# Node ID f319054e8dffd908d220e7058a82900b08d89c70
# Parent  f4e9bd04e1d50ef116f766664d8aed70d249f80a
removed redundant code line

diff -r f4e9bd04e1d5 -r f319054e8dff 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