tuned;
authorwenzelm
Thu May 11 19:19:33 2006 +0200 (2006-05-11)
changeset 196189050a3b01e62
parent 19617 7cb4b67d4b97
child 19619 ee1104f972a4
tuned;
src/Provers/Arith/fast_lin_arith.ML
src/Pure/Isar/local_syntax.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu May 11 19:19:31 2006 +0200
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu May 11 19:19:33 2006 +0200
     1.3 @@ -364,7 +364,7 @@
     1.4           val c = hd sclist
     1.5           val (SOME(eq as Lineq(_,_,ceq,_)),othereqs) =
     1.6                 extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
     1.7 -         val v = find_index_eq c ceq
     1.8 +         val v = find_index (fn x => x = c) ceq
     1.9           val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => el v l = 0)
    1.10                                       (othereqs @ noneqs)
    1.11           val others = map (elim_var v eq) roth @ ioth
     2.1 --- a/src/Pure/Isar/local_syntax.ML	Thu May 11 19:19:31 2006 +0200
     2.2 +++ b/src/Pure/Isar/local_syntax.ML	Thu May 11 19:19:33 2006 +0200
     2.3 @@ -126,7 +126,7 @@
     2.4    let
     2.5      val (structs, fixes) = idents_of syntax;
     2.6      fun map_free (t as Free (x, T)) =
     2.7 -          let val i = Library.find_index_eq x structs + 1 in
     2.8 +          let val i = find_index (fn s => s = x) structs + 1 in
     2.9              if i = 0 andalso member (op =) fixes x then
    2.10                Const (Syntax.fixedN ^ x, T)
    2.11              else if i = 1 andalso not (! show_structs) then
     3.1 --- a/src/Pure/Proof/proof_syntax.ML	Thu May 11 19:19:31 2006 +0200
     3.2 +++ b/src/Pure/Proof/proof_syntax.ML	Thu May 11 19:19:33 2006 +0200
     3.3 @@ -113,7 +113,7 @@
     3.4              val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s);
     3.5              val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s)))
     3.6            in if prop = prop' then prf' else
     3.7 -            PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags),
     3.8 +            PThm ((s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps), tags),
     3.9                prf, prop, Ts)
    3.10            end
    3.11        | rename prf = prf
     4.1 --- a/src/Pure/meta_simplifier.ML	Thu May 11 19:19:31 2006 +0200
     4.2 +++ b/src/Pure/meta_simplifier.ML	Thu May 11 19:19:33 2006 +0200
     4.3 @@ -1100,7 +1100,7 @@
     4.4                val prem' = rhs_of eqn;
     4.5                val tprems = map term_of prems;
     4.6                val i = 1 + Library.foldl Int.max (~1, map (fn p =>
     4.7 -                find_index_eq p tprems) (#hyps (rep_thm eqn)));
     4.8 +                find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
     4.9                val (rrs', asm') = rules_of_prem ss prem'
    4.10              in mut_impc prems concl rrss asms (prem' :: prems')
    4.11                (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)