changeset 18964 | 67f572e03236 |
parent 18938 | b401ee1cda14 |
child 19071 | fdffd7c40864 |
--- a/src/Pure/logic.ML Tue Feb 07 08:47:43 2006 +0100 +++ b/src/Pure/logic.ML Tue Feb 07 19:56:45 2006 +0100 @@ -223,7 +223,7 @@ | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t; val lhs_bads = filter_out check_arg args; - val lhs_dups = gen_duplicates (op aconv) args; + val lhs_dups = duplicates (op aconv) args; val rhs_extras = Term.fold_aterms (fn v as Free (x, _) => if is_fixed x orelse member (op aconv) args v then I else insert (op aconv) v | _ => I) rhs [];