--- a/src/FOL/simpdata.ML Fri Nov 07 17:51:26 1997 +0100
+++ b/src/FOL/simpdata.ML Fri Nov 07 18:02:15 1997 +0100
@@ -247,16 +247,11 @@
fun is_eq (Const ("Trueprop", _) $ (Const("op =" ,_) $ _ $ _)) = true
| is_eq (Const ("Trueprop", _) $ (Const("op <->",_) $ _ $ _)) = true
| is_eq _ = false;
- fun find_eq n [] = None
- | find_eq n (t :: ts) = if (is_eq t) then Some n
- else find_eq (n + 1) ts;
+ val find_eq = find_index is_eq;
in
val rot_eq_tac =
- SUBGOAL (fn (Bi,i) =>
- case find_eq 0 (Logic.strip_assums_hyp Bi) of
- None => no_tac
- | Some 0 => no_tac
- | Some n => rotate_tac n i)
+ SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
+ if n>0 then rotate_tac n i else no_tac end)
end;
--- a/src/HOL/datatype.ML Fri Nov 07 17:51:26 1997 +0100
+++ b/src/HOL/datatype.ML Fri Nov 07 18:02:15 1997 +0100
@@ -194,7 +194,7 @@
| trans_recs' cis (eq::eqs) =
let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq;
val tc = assoc(tcs,c);
- val i = (1 + find (c,cs)) handle LIST "find" => 0;
+ val i = 1 + find_index_eq c cs;
in
if name <> name1 then
raise RecError "function names inconsistent"
--- a/src/HOL/simpdata.ML Fri Nov 07 17:51:26 1997 +0100
+++ b/src/HOL/simpdata.ML Fri Nov 07 18:02:15 1997 +0100
@@ -456,16 +456,11 @@
local
fun is_eq (Const ("Trueprop", _) $ (Const("op =" ,_) $ _ $ _)) = true
| is_eq _ = false;
- fun find_eq n [] = None
- | find_eq n (t :: ts) = if (is_eq t) then Some n
- else find_eq (n + 1) ts;
+ val find_eq = find_index is_eq;
in
val rot_eq_tac =
- SUBGOAL (fn (Bi,i) =>
- case find_eq 0 (Logic.strip_assums_hyp Bi) of
- None => no_tac
- | Some 0 => no_tac
- | Some n => rotate_tac n i)
+ SUBGOAL (fn (Bi,i) => let val n = find_eq (Logic.strip_assums_hyp Bi) in
+ if n>0 then rotate_tac n i else no_tac end)
end;
(*an unsatisfactory fix for the incomplete asm_full_simp_tac!
--- a/src/HOLCF/domain/extender.ML Fri Nov 07 17:51:26 1997 +0100
+++ b/src/HOLCF/domain/extender.ML Fri Nov 07 18:02:15 1997 +0100
@@ -84,14 +84,14 @@
val eqs' = check_and_sort_domain (dtnvs,cons'') sg'';
val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
val dts = map (Type o fst) eqs';
- fun strip ss = drop (find ("'", ss)+1, ss);
+ fun strip ss = drop (find_index_eq "'" ss +1, ss);
fun typid (Type (id,_) ) = hd (explode (Sign.base_name id))
| typid (TFree (id,_) ) = hd (strip (tl (explode (Sign.base_name id))))
| typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
fun cons cons' = (map (fn (con,syn,args) =>
((Syntax.const_name con syn),
ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
- find (tp,dts) handle LIST "find" => ~1),
+ find_index_eq tp dts),
sel,vn))
(args,(mk_var_names(map (typid o third) args)))
)) cons') : cons list;
--- a/src/HOLCF/domain/library.ML Fri Nov 07 17:51:26 1997 +0100
+++ b/src/HOLCF/domain/library.ML Fri Nov 07 18:02:15 1997 +0100
@@ -168,7 +168,7 @@
fun defined t = t ~= UU;
fun cpair (S,T) = %%"cpair"`S`T;
fun lift_defined f = lift (fn x => defined (f x));
-fun bound_arg vns v = Bound(length vns-find(v,vns)-1);
+fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) =
(case cont_eta_contract body of
--- a/src/Pure/library.ML Fri Nov 07 17:51:26 1997 +0100
+++ b/src/Pure/library.ML Fri Nov 07 18:02:15 1997 +0100
@@ -245,10 +245,11 @@
(*find the position of an element in a list*)
-fun find (x, ys) =
- let fun f (y :: ys, i) = if x = y then i else f (ys, i + 1)
- | f (_, _) = raise LIST "find"
- in f (ys, 0) end;
+fun find_index (pred: 'a->bool) : 'a list -> int =
+ let fun find _ [] = ~1
+ | find n (x::xs) = if pred x then n else find (n+1) xs
+ in find 0 end;
+fun find_index_eq x = find_index (fn y => y = x);
(*flatten a list of lists to a list*)
fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
@@ -294,10 +295,10 @@
| Some y => y :: mapfilter f xs);
-fun find_first _ [] = None
- | find_first pred (x :: xs) =
- if pred x then Some x else find_first pred xs;
-
+fun find_first pred = let
+ fun f [] = None
+ | f (x :: xs) = if pred x then Some x else f xs
+ in f end;
(* lists of pairs *)
--- a/src/Pure/term.ML Fri Nov 07 17:51:26 1997 +0100
+++ b/src/Pure/term.ML Fri Nov 07 18:02:15 1997 +0100
@@ -715,6 +715,7 @@
val memo_types = ref (Symtab.null : typ list Symtab.table);
+(* special case of library/find_first *)
fun find_type (T, []: typ list) = None
| find_type (T, T'::Ts) =
if T=T' then Some T'
@@ -744,6 +745,7 @@
val memo_terms = ref (Symtab.null : term list Symtab.table);
+(* special case of library/find_first *)
fun find_term (t, []: term list) = None
| find_term (t, t'::ts) =
if t=t' then Some t'