removed obsolete first_duplicate;
authorwenzelm
Sun Nov 05 21:44:35 2006 +0100 (2006-11-05)
changeset 21182747ff99b35ee
parent 21181 13c3fdccdf0d
child 21183 a76f457b6d86
removed obsolete first_duplicate;
src/Pure/library.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/library.ML	Sun Nov 05 21:44:34 2006 +0100
     1.2 +++ b/src/Pure/library.ML	Sun Nov 05 21:44:35 2006 +0100
     1.3 @@ -220,7 +220,6 @@
     1.4    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
     1.5    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
     1.6    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
     1.7 -  val first_duplicate: ('a * 'a -> bool) -> 'a list -> 'a option
     1.8  
     1.9    (*lists as tables -- see also Pure/General/alist.ML*)
    1.10    val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    1.11 @@ -1051,11 +1050,6 @@
    1.12        | dups (x :: xs) = member eq xs x orelse dups xs;
    1.13    in dups end;
    1.14  
    1.15 -fun first_duplicate eq =
    1.16 -  let
    1.17 -    fun dup [] = NONE
    1.18 -      | dup (x :: xs) = if member eq xs x then SOME x else dup xs;
    1.19 -  in dup end;
    1.20  
    1.21  (** association lists -- legacy operations **)
    1.22  
     2.1 --- a/src/Pure/thm.ML	Sun Nov 05 21:44:34 2006 +0100
     2.2 +++ b/src/Pure/thm.ML	Sun Nov 05 21:44:35 2006 +0100
     2.3 @@ -1376,9 +1376,9 @@
     2.4      val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
     2.5      val newBi = Logic.list_rename_params (newnames, Bi);
     2.6    in
     2.7 -    case first_duplicate (op =) cs of
     2.8 -      SOME c => (warning ("Can't rename.  Bound variables not distinct: " ^ c); state)
     2.9 -    | NONE =>
    2.10 +    (case duplicates (op =) cs of
    2.11 +      a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
    2.12 +    | [] =>
    2.13        (case cs inter_string freenames of
    2.14          a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
    2.15        | [] =>
    2.16 @@ -1388,7 +1388,7 @@
    2.17            shyps = shyps,
    2.18            hyps = hyps,
    2.19            tpairs = tpairs,
    2.20 -          prop = Logic.list_implies (Bs @ [newBi], C)})
    2.21 +          prop = Logic.list_implies (Bs @ [newBi], C)}))
    2.22    end;
    2.23  
    2.24