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