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