# HG changeset patch
# User wenzelm
# Date 1425498449 -3600
# Node ID 4517e9a96aceccacd6f9dad6238219b8328905e7
# Parent  3c94c44dfc0f4ae712d993e822332f670bd6ca00
tuned;

diff -r 3c94c44dfc0f -r 4517e9a96ace src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Mar 04 20:16:39 2015 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Wed Mar 04 20:47:29 2015 +0100
@@ -199,7 +199,7 @@
                   let
                     val (j, b) :: rest = lq
                     val (i, a) = the (covering g strict j)
-                    fun choose xs = set_member_tac (Library.find_index (curry op = (i, a)) xs) 1
+                    fun choose xs = set_member_tac (find_index (curry op = (i, a)) xs) 1
                     val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
                   in
                     rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
@@ -216,7 +216,7 @@
                   let
                     val (i, a) :: rest = lp
                     val (j, b) = the (covering g strict i)
-                    fun choose xs = set_member_tac (Library.find_index (curry op = (j, b)) xs) 1
+                    fun choose xs = set_member_tac (find_index (curry op = (j, b)) xs) 1
                     val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
                   in
                     rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
@@ -231,7 +231,7 @@
                 val qs = subtract (op =) (map_filter get_str_cover lq) lq
                 val ps = map get_wk_cover qs
 
-                fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
+                fun indices xs ys = map (fn y => find_index (curry op = y) xs) ys
                 val iqs = indices lq qs
                 val ips = indices lp ps
 
diff -r 3c94c44dfc0f -r 4517e9a96ace src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 04 20:16:39 2015 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Wed Mar 04 20:47:29 2015 +0100
@@ -404,7 +404,7 @@
   let val _ = print_ineqs ctxt ineqs
       val (triv, nontriv) = List.partition is_trivial ineqs in
   if not (null triv)
-  then case Library.find_first is_contradictory triv of
+  then case find_first is_contradictory triv of
          NONE => elim ctxt (nontriv, hist)
        | SOME(Lineq(_,_,_,j)) => Success j
   else
diff -r 3c94c44dfc0f -r 4517e9a96ace src/Provers/order.ML
--- a/src/Provers/order.ML	Wed Mar 04 20:16:39 2015 +0100
+++ b/src/Provers/order.ML	Wed Mar 04 20:47:29 2015 +0100
@@ -980,7 +980,7 @@
   if null neqE then raise Cannot
   (* if there aren't any edges that are candidate for <= then just search a edge in neqE that implies the subgoal *)
   else if null sccSubgraphs then (
-     (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
+     (case (find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
        ( SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
           if  (x aconv x' andalso y aconv y') then p
           else Thm ([p], #not_sym less_thms)
diff -r 3c94c44dfc0f -r 4517e9a96ace src/Provers/quasi.ML
--- a/src/Provers/quasi.ML	Wed Mar 04 20:16:39 2015 +0100
+++ b/src/Provers/quasi.ML	Wed Mar 04 20:47:29 2015 +0100
@@ -482,7 +482,7 @@
    end )
  | (NotEq (x,y,_)) =>
   (* First check if a single premiss is sufficient *)
-  (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
+  (case (find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
     (SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
       if  (x aconv x' andalso y aconv y') then p
       else Thm ([p], @{thm not_sym})
diff -r 3c94c44dfc0f -r 4517e9a96ace src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Mar 04 20:16:39 2015 +0100
+++ b/src/Pure/tactic.ML	Wed Mar 04 20:47:29 2015 +0100
@@ -294,7 +294,7 @@
 
 (*Renaming of parameters in a subgoal*)
 fun rename_tac xs i =
-  case Library.find_first (not o Symbol_Pos.is_identifier) xs of
+  case find_first (not o Symbol_Pos.is_identifier) xs of
       SOME x => error ("Not an identifier: " ^ x)
     | NONE => PRIMITIVE (Thm.rename_params_rule (xs, i));