--- a/src/Pure/theory.ML Wed Nov 09 16:26:53 2005 +0100
+++ b/src/Pure/theory.ML Wed Nov 09 16:26:54 2005 +0100
@@ -273,8 +273,8 @@
val show_tfrees = commas_quote o map fst;
val lhs_nofrees = filter (not o can dest_free) args;
- val lhs_dups = duplicates args;
- val rhs_extras = term_frees rhs |> fold (remove op =) args;
+ val lhs_dups = gen_duplicates (op aconv) args;
+ val rhs_extras = term_frees rhs |> fold (remove op aconv) args;
val rhs_extrasT = term_tfrees rhs |> fold (remove op =) (typ_tfrees T);
in
if not (null lhs_nofrees) then