author | blanchet |
Wed, 19 Nov 2014 10:31:15 +0100 | |
changeset 59013 | f319054e8dff |
parent 59012 | f4e9bd04e1d5 |
child 59014 | cc5e34575354 |
--- 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