--- 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
--- 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
--- 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)
--- 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})
--- 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));