diff -r 3adfc9dfb30a -r 67f572e03236 src/Pure/logic.ML
--- 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 [];