--- a/src/HOL/Tools/meson.ML Wed Oct 11 10:49:29 2006 +0200
+++ b/src/HOL/Tools/meson.ML Wed Oct 11 10:49:36 2006 +0200
@@ -273,8 +273,9 @@
(*Remove duplicate literals, if there are any*)
fun nodups th =
- if null(findrep(literals(prop_of th))) then th
- else nodups_aux [] th;
+ if has_duplicates (op =) (literals (prop_of th))
+ then nodups_aux [] th
+ else th;
(**** Generation of contrapositives ****)
--- a/src/Pure/library.ML Wed Oct 11 10:49:29 2006 +0200
+++ b/src/Pure/library.ML Wed Oct 11 10:49:36 2006 +0200
@@ -219,10 +219,10 @@
val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
val \ : ''a list * ''a -> ''a list
val \\ : ''a list * ''a list -> ''a list
- val findrep: ''a list -> ''a list
val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
+ val first_duplicate: ('a * 'a -> bool) -> 'a list -> 'a option
(*lists as tables -- see also Pure/General/alist.ML*)
val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
@@ -1036,11 +1036,6 @@
fun ys \\ xs = foldl (op \) (ys,xs);
-(*returns the tail beginning with the first repeated element, or []*)
-fun findrep [] = []
- | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
-
-
(*makes a list of the distinct members of the input; preserves order, takes
first of equal elements*)
fun distinct eq lst =
@@ -1068,6 +1063,11 @@
| dups (x :: xs) = member eq xs x orelse dups xs;
in dups end;
+fun first_duplicate eq =
+ let
+ fun dup [] = NONE
+ | dup (x :: xs) = if member eq xs x then SOME x else dup xs;
+ in dup end;
(** association lists -- legacy operations **)
--- a/src/Pure/meta_simplifier.ML Wed Oct 11 10:49:29 2006 +0200
+++ b/src/Pure/meta_simplifier.ML Wed Oct 11 10:49:36 2006 +0200
@@ -549,7 +549,7 @@
Const ("==", _) $ lhs $ rhs =>
let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
is_Var x andalso forall is_Bound xs andalso
- null (findrep xs) andalso xs = ys andalso
+ not (has_duplicates (op =) xs) andalso xs = ys andalso
member (op =) varpairs (x, y) andalso
is_full_cong_prems prems (remove (op =) (x, y) varpairs)
end
@@ -561,7 +561,7 @@
val (lhs, rhs) = Logic.dest_equals concl;
val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
in
- f = g andalso null (findrep (xs @ ys)) andalso length xs = length ys andalso
+ f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
is_full_cong_prems prems (xs ~~ ys)
end;
--- a/src/Pure/thm.ML Wed Oct 11 10:49:29 2006 +0200
+++ b/src/Pure/thm.ML Wed Oct 11 10:49:36 2006 +0200
@@ -1376,9 +1376,9 @@
val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
val newBi = Logic.list_rename_params (newnames, Bi);
in
- case findrep cs of
- c :: _ => (warning ("Can't rename. Bound variables not distinct: " ^ c); state)
- | [] =>
+ case first_duplicate (op =) cs of
+ SOME c => (warning ("Can't rename. Bound variables not distinct: " ^ c); state)
+ | NONE =>
(case cs inter_string freenames of
a :: _ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); state)
| [] =>