# HG changeset patch # User haftmann # Date 1247205567 -7200 # Node ID a68f88d264f75e57c1de5da5a2be586101403784 # Parent a6e982b1ebba579b6802932dde9b5f71bb9bbebd dropped find_index_eq diff -r a6e982b1ebba -r a68f88d264f7 src/HOL/Library/comm_ring.ML --- 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) diff -r a6e982b1ebba -r a68f88d264f7 src/HOL/Library/reflection.ML --- 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, diff -r a6e982b1ebba -r a68f88d264f7 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- 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))); diff -r a6e982b1ebba -r a68f88d264f7 src/HOL/Tools/inductive.ML --- 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) diff -r a6e982b1ebba -r a68f88d264f7 src/HOL/Tools/inductive_realizer.ML --- 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)) => diff -r a6e982b1ebba -r a68f88d264f7 src/HOL/Tools/refute.ML --- 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 diff -r a6e982b1ebba -r a68f88d264f7 src/HOL/ex/predicate_compile.ML --- 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')) diff -r a6e982b1ebba -r a68f88d264f7 src/HOLCF/Tools/domain/domain_extender.ML --- 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 diff -r a6e982b1ebba -r a68f88d264f7 src/HOLCF/Tools/domain/domain_library.ML --- 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 diff -r a6e982b1ebba -r a68f88d264f7 src/Provers/Arith/fast_lin_arith.ML --- 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 diff -r a6e982b1ebba -r a68f88d264f7 src/Pure/library.ML --- 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;