--- a/src/HOL/Library/comm_ring.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/HOL/Library/comm_ring.ML Fri Jul 10 07:59:27 2009 +0200
@@ -41,7 +41,7 @@
fun reif_pol T vs (t as Free _) =
let
val one = @{term "1::nat"};
- val i = find_index_eq t vs
+ val i = find_index (fn t' => t' = t) vs
in if i = 0
then pol_PX T $ (pol_Pc T $ cring_one T)
$ one $ (pol_Pc T $ cring_zero T)
--- a/src/HOL/Library/reflection.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/HOL/Library/reflection.ML Fri Jul 10 07:59:27 2009 +0200
@@ -103,8 +103,8 @@
NONE => error "index_of : type not found in environements!"
| SOME (tbs,tats) =>
let
- val i = find_index_eq t tats
- val j = find_index_eq t tbs
+ val i = find_index (fn t' => t' = t) tats
+ val j = find_index (fn t' => t' = t) tbs
in (if j = ~1 then
if i = ~1
then (length tbs + length tats,
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Jul 10 07:59:27 2009 +0200
@@ -111,7 +111,7 @@
else
Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
end
- in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs)
+ in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
end;
(* make injections for constructors *)
@@ -137,7 +137,7 @@
if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
end
- in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
+ in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs)
end;
val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
--- a/src/HOL/Tools/inductive.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Jul 10 07:59:27 2009 +0200
@@ -222,7 +222,7 @@
val k = length params;
val (c, ts) = strip_comb t;
val (xs, ys) = chop k ts;
- val i = find_index_eq c cs;
+ val i = find_index (fn c' => c' = c) cs;
in
if xs = params andalso i >= 0 then
SOME (c, i, ys, chop (length ys)
--- a/src/HOL/Tools/inductive_realizer.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Jul 10 07:59:27 2009 +0200
@@ -204,9 +204,9 @@
fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
let
val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
- val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
- SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
- find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
+ val premss = map_filter (fn (s, rs) => if member (op =) rsets s then
+ SOME (rs, map (fn (_, r) => nth (prems_of raw_induct)
+ (find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss;
val fs = maps (fn ((intrs, prems), dummy) =>
let
val fs = map (fn (rule, (ivs, intr)) =>
--- a/src/HOL/Tools/refute.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/HOL/Tools/refute.ML Fri Jul 10 07:59:27 2009 +0200
@@ -2401,7 +2401,7 @@
(* by our assumption on the order of recursion operators *)
(* and datatypes, this is the index of the datatype *)
(* corresponding to the given recursion operator *)
- val idt_index = find_index_eq s (#rec_names info)
+ val idt_index = find_index (fn s' => s' = s) (#rec_names info)
(* mutually recursive types must have the same type *)
(* parameters, unless the mutual recursion comes from *)
(* indirect recursion *)
@@ -2535,7 +2535,7 @@
(* returned *)
(* interpretation -> int -> int list option *)
fun get_args (Leaf xs) elem =
- if find_index_eq True xs = elem then
+ if find_index (fn x => x = True) xs = elem then
SOME []
else
NONE
@@ -2606,7 +2606,7 @@
(* corresponding recursive argument *)
fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
(* recursive argument is "rec_i params elem" *)
- compute_array_entry i (find_index_eq True xs)
+ compute_array_entry i (find_index (fn x => x = True) xs)
| rec_intr (DatatypeAux.DtRec _) (Node _) =
raise REFUTE ("IDT_recursion_interpreter",
"interpretation for IDT is a node")
@@ -3237,7 +3237,7 @@
def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
(* interpretation -> int list option *)
fun get_args (Leaf xs) =
- if find_index_eq True xs = element then
+ if find_index (fn x => x = True) xs = element then
SOME []
else
NONE
--- a/src/HOL/ex/predicate_compile.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Fri Jul 10 07:59:27 2009 +0200
@@ -419,8 +419,8 @@
error ("Too few arguments for inductive predicate " ^ name)
else chop (length iss) args;
val k = length args2;
- val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1)
- (1 upto b)
+ val perm = map (fn i => (find_index (fn t => t = Bound (b - i)) args2) + 1)
+ (1 upto b)
val partial_mode = (1 upto k) \\ perm
in
if not (partial_mode subset is) then [] else
@@ -627,7 +627,7 @@
val (params, args') = chop (length ms) args
val (inargs, outargs) = get_args is' args'
val b = length vs
- val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b)
+ val perm = map (fn i => find_index (fn t => t = Bound (b - i)) args' + 1) (1 upto b)
val outp_perm =
snd (get_args is perm)
|> map (fn i => i - length (filter (fn x => x < i) is'))
--- a/src/HOLCF/Tools/domain/domain_extender.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_extender.ML Fri Jul 10 07:59:27 2009 +0200
@@ -121,7 +121,7 @@
val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
val dts = map (Type o fst) eqs';
val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
- fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
+ fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
fun typid (Type (id,_)) =
let val c = hd (Symbol.explode (Long_Name.base_name id))
in if Symbol.is_letter c then c else "t" end
--- a/src/HOLCF/Tools/domain/domain_library.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/HOLCF/Tools/domain/domain_library.ML Fri Jul 10 07:59:27 2009 +0200
@@ -365,7 +365,7 @@
fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2;
val mk_ctuple_pat = foldr1 cpair_pat;
fun lift_defined f = lift (fn x => defined (f x));
-fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
+fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);
fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) =
(case cont_eta_contract body of
--- a/src/Provers/Arith/fast_lin_arith.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri Jul 10 07:59:27 2009 +0200
@@ -391,7 +391,7 @@
|> hd
val (eq as Lineq(_,_,ceq,_),othereqs) =
extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
- val v = find_index_eq c ceq
+ val v = find_index (fn v => v = c) ceq
val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0)
(othereqs @ noneqs)
val others = map (elim_var v eq) roth @ ioth
--- a/src/Pure/library.ML Fri Jul 10 07:59:25 2009 +0200
+++ b/src/Pure/library.ML Fri Jul 10 07:59:27 2009 +0200
@@ -97,7 +97,6 @@
val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
val split_last: 'a list -> 'a list * 'a
val find_index: ('a -> bool) -> 'a list -> int
- val find_index_eq: ''a -> ''a list -> int
val find_first: ('a -> bool) -> 'a list -> 'a option
val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
val get_first: ('a -> 'b option) -> 'a list -> 'b option
@@ -503,8 +502,6 @@
| find n (x :: xs) = if pred x then n else find (n + 1) xs;
in find 0 end;
-fun find_index_eq x = find_index (equal x);
-
(*find first element satisfying predicate*)
val find_first = List.find;