src/Pure/logic.ML

       | check_arg _ = false;
     fun close_arg (Bound _) t = t
       | 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 [];
     val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
       if is_fixedT a orelse member (op =) head_tfrees (a, S) then I