--- a/src/Provers/Arith/fast_lin_arith.ML Thu May 11 19:19:31 2006 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu May 11 19:19:33 2006 +0200
@@ -364,7 +364,7 @@
val c = hd sclist
val (SOME(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 x => x = c) ceq
val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => el v l = 0)
(othereqs @ noneqs)
val others = map (elim_var v eq) roth @ ioth
--- a/src/Pure/Isar/local_syntax.ML Thu May 11 19:19:31 2006 +0200
+++ b/src/Pure/Isar/local_syntax.ML Thu May 11 19:19:33 2006 +0200
@@ -126,7 +126,7 @@
let
val (structs, fixes) = idents_of syntax;
fun map_free (t as Free (x, T)) =
- let val i = Library.find_index_eq x structs + 1 in
+ let val i = find_index (fn s => s = x) structs + 1 in
if i = 0 andalso member (op =) fixes x then
Const (Syntax.fixedN ^ x, T)
else if i = 1 andalso not (! show_structs) then
--- a/src/Pure/Proof/proof_syntax.ML Thu May 11 19:19:31 2006 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Thu May 11 19:19:33 2006 +0200
@@ -113,7 +113,7 @@
val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s);
val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s)))
in if prop = prop' then prf' else
- PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
+ PThm ((s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps), tags),
prf, prop, Ts)
end
| rename prf = prf
--- a/src/Pure/meta_simplifier.ML Thu May 11 19:19:31 2006 +0200
+++ b/src/Pure/meta_simplifier.ML Thu May 11 19:19:33 2006 +0200
@@ -1100,7 +1100,7 @@
val prem' = rhs_of eqn;
val tprems = map term_of prems;
val i = 1 + Library.foldl Int.max (~1, map (fn p =>
- find_index_eq p tprems) (#hyps (rep_thm eqn)));
+ find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
val (rrs', asm') = rules_of_prem ss prem'
in mut_impc prems concl rrss asms (prem' :: prems')
(rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)