changeset 42083 | e1209fc7ecdc |
parent 41228 | e1fce873b814 |
child 42361 | 23f352990944 |
--- a/src/Tools/atomize_elim.ML Thu Mar 24 16:47:24 2011 +0100 +++ b/src/Tools/atomize_elim.ML Thu Mar 24 16:56:19 2011 +0100 @@ -80,7 +80,7 @@ fun movea_conv ctxt ct = let val _ $ Abs (_, _, b) = term_of ct - val idxs = fold_index (fn (i, t) => not (loose_bvar1 (t, 0)) ? cons i) + val idxs = fold_index (fn (i, t) => not (Term.is_dependent t) ? cons i) (Logic.strip_imp_prems b) [] |> rev