1.1 --- a/src/HOL/Tools/meson.ML	Wed Oct 11 10:49:29 2006 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Oct 11 10:49:36 2006 +0200
     1.3 @@ -273,8 +273,9 @@
     1.4  
     1.5  (*Remove duplicate literals, if there are any*)
     1.6  fun nodups th =
     1.7 -    if null(findrep(literals(prop_of th))) then th
     1.8 -    else nodups_aux [] th;
     1.9 +  if has_duplicates (op =) (literals (prop_of th))
    1.10 +    then nodups_aux [] th
    1.11 +    else th;
    1.12  
    1.13  
    1.14  (**** Generation of contrapositives ****)

     2.1 --- a/src/Pure/library.ML	Wed Oct 11 10:49:29 2006 +0200
     2.2 +++ b/src/Pure/library.ML	Wed Oct 11 10:49:36 2006 +0200
     2.3 @@ -219,10 +219,10 @@
     2.4    val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     2.5    val \ : ''a list * ''a -> ''a list
     2.6    val \\ : ''a list * ''a list -> ''a list
     2.7 -  val findrep: ''a list -> ''a list
     2.8    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
     2.9    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
    2.10    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
    2.11 +  val first_duplicate: ('a * 'a -> bool) -> 'a list -> 'a option
    2.12  
    2.13    (*lists as tables -- see also Pure/General/alist.ML*)
    2.14    val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    2.15 @@ -1036,11 +1036,6 @@
    2.16  fun ys \\ xs = foldl (op \) (ys,xs);
    2.17  
    2.18  
    2.19 -(*returns the tail beginning with the first repeated element, or []*)
    2.20 -fun findrep [] = []
    2.21 -  | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
    2.22 -
    2.23 -
    2.24  (*makes a list of the distinct members of the input; preserves order, takes
    2.25    first of equal elements*)
    2.26  fun distinct eq lst =
    2.27 @@ -1068,6 +1063,11 @@
    2.28        | dups (x :: xs) = member eq xs x orelse dups xs;
    2.29    in dups end;
    2.30  
    2.31 +fun first_duplicate eq =
    2.32 +  let
    2.33 +    fun dup [] = NONE
    2.34 +      | dup (x :: xs) = if member eq xs x then SOME x else dup xs;
    2.35 +  in dup end;
    2.36  
    2.37  (** association lists -- legacy operations **)
    2.38  

     3.1 --- a/src/Pure/meta_simplifier.ML	Wed Oct 11 10:49:29 2006 +0200
     3.2 +++ b/src/Pure/meta_simplifier.ML	Wed Oct 11 10:49:36 2006 +0200
     3.3 @@ -549,7 +549,7 @@
     3.4          Const ("==", _) $ lhs $ rhs =>
     3.5            let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
     3.6              is_Var x andalso forall is_Bound xs andalso
     3.7 -            null (findrep xs) andalso xs = ys andalso
     3.8 +            not (has_duplicates (op =) xs) andalso xs = ys andalso
     3.9              member (op =) varpairs (x, y) andalso
    3.10              is_full_cong_prems prems (remove (op =) (x, y) varpairs)
    3.11            end
    3.12 @@ -561,7 +561,7 @@
    3.13      val (lhs, rhs) = Logic.dest_equals concl;
    3.14      val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
    3.15    in
    3.16 -    f = g andalso null (findrep (xs @ ys)) andalso length xs = length ys andalso
    3.17 +    f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
    3.18      is_full_cong_prems prems (xs ~~ ys)
    3.19    end;
    3.20  

     4.1 --- a/src/Pure/thm.ML	Wed Oct 11 10:49:29 2006 +0200
     4.2 +++ b/src/Pure/thm.ML	Wed Oct 11 10:49:36 2006 +0200
     4.3 @@ -1376,9 +1376,9 @@
     4.4      val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
     4.5      val newBi = Logic.list_rename_params (newnames, Bi);
     4.6    in
     4.7 -    case findrep cs of
     4.8 -      c :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ c); state)
     4.9 -    | [] =>
    4.10 +    case first_duplicate (op =) cs of
    4.11 +      SOME c => (warning ("Can't rename.  Bound variables not distinct: " ^ c); state)
    4.12 +    | NONE =>
    4.13        (case cs inter_string freenames of
    4.14          a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
    4.15        | [] =>