src/Pure/theory.ML
changeset 18139 b15981aedb7b
parent 17706 e534e39f3531
child 18338 ed2d0e60fbcc
     1.1 --- a/src/Pure/theory.ML	Wed Nov 09 16:26:53 2005 +0100
     1.2 +++ b/src/Pure/theory.ML	Wed Nov 09 16:26:54 2005 +0100
     1.3 @@ -273,8 +273,8 @@
     1.4      val show_tfrees = commas_quote o map fst;
     1.5  
     1.6      val lhs_nofrees = filter (not o can dest_free) args;
     1.7 -    val lhs_dups = duplicates args;
     1.8 -    val rhs_extras = term_frees rhs |> fold (remove op =) args;
     1.9 +    val lhs_dups = gen_duplicates (op aconv) args;
    1.10 +    val rhs_extras = term_frees rhs |> fold (remove op aconv) args;
    1.11      val rhs_extrasT = term_tfrees rhs |> fold (remove op =) (typ_tfrees T);
    1.12    in
    1.13      if not (null lhs_nofrees) then