# HG changeset patch
# User wenzelm
# Date 1147367973 -7200
# Node ID 9050a3b01e626da78173a17931920d3c630531b2
# Parent  7cb4b67d4b979a1264261009dbbbcba94ebd2d1d
tuned;

diff -r 7cb4b67d4b97 -r 9050a3b01e62 src/Provers/Arith/fast_lin_arith.ML
--- 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
diff -r 7cb4b67d4b97 -r 9050a3b01e62 src/Pure/Isar/local_syntax.ML
--- 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
diff -r 7cb4b67d4b97 -r 9050a3b01e62 src/Pure/Proof/proof_syntax.ML
--- 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
diff -r 7cb4b67d4b97 -r 9050a3b01e62 src/Pure/meta_simplifier.ML
--- 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)