# HG changeset patch
# User oheimb
# Date 878922135 -3600
# Node ID 1025a27b08f942d63465160df482472cfed25775
# Parent  2fafec5868fe7f9b02f9b1c6fb40657bbfa81877
changed libraray function find to find_index_eq, currying it

diff -r 2fafec5868fe -r 1025a27b08f9 src/FOL/simpdata.ML
--- 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;
 
 
diff -r 2fafec5868fe -r 1025a27b08f9 src/HOL/datatype.ML
--- 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"
diff -r 2fafec5868fe -r 1025a27b08f9 src/HOL/simpdata.ML
--- 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!
diff -r 2fafec5868fe -r 1025a27b08f9 src/HOLCF/domain/extender.ML
--- 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;
diff -r 2fafec5868fe -r 1025a27b08f9 src/HOLCF/domain/library.ML
--- 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
diff -r 2fafec5868fe -r 1025a27b08f9 src/Pure/library.ML
--- 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 *)
 
diff -r 2fafec5868fe -r 1025a27b08f9 src/Pure/term.ML
--- 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'