src/HOLCF/adm.ML

 
 fun find_subterms (Bound i) lev path =
       if i = lev then [[(Bound 0, path)]]
       else []
   | find_subterms (t as (Abs (_, _, t2))) lev path =
-      if filter (fn x => x<=lev)
+      if List.filter (fn x => x<=lev)
            (add_loose_bnos (t, 0, [])) = [lev] then
         [(incr_bv (~lev, 0, t), path)]::
         (find_subterms t2 (lev+1) (0::path))
       else find_subterms t2 (lev+1) (0::path)
   | find_subterms (t as (t1 $ t2)) lev path =

           val ts2 = find_subterms t2 lev (1::path);
           fun combine [] y = []
             | combine (x::xs) ys =
                 (map (fn z => x @ z) ys) @ (combine xs ys)
       in
-        (if filter (fn x => x<=lev)
+        (if List.filter (fn x => x<=lev)
               (add_loose_bnos (t, 0, [])) = [lev] then
            [[(incr_bv (~lev, 0, t), path)]]
          else []) @
         (if ts1 = [] then ts2
          else if ts2 = [] then ts1

   let val {sign, maxidx, ...} = rep_thm state;
       val j = maxidx+1;
       val tsig = Sign.tsig_of sign;
       val parTs = map snd (rev params);
       val rule = lift_rule (state, i) adm_subst;
-      val types = the o (fst (types_sorts rule));
+      val types = valOf o (fst (types_sorts rule));
       val tT = types ("t", j);
       val PT = types ("P", j);
       fun mk_abs [] t = t
         | mk_abs ((a,T)::Ts) t = Abs (a, T, mk_abs Ts t);
       val tt = cterm_of sign (mk_abs (params @ [(s, T)]) subt);

   in rule' end;
 
 
 (*** extract subgoal i from proof state ***)
 
-fun nth_subgoal i thm = nth_elem (i-1, prems_of thm);
+fun nth_subgoal i thm = List.nth (prems_of thm, i-1);
 
 
 (*** the admissibility tactic ***)
 
 fun try_dest_adm (Const _ $ (Const (name, _) $ Abs abs)) =

         let
           val sign = sign_of_thm state;
           val prems = Logic.strip_assums_hyp goali;
           val params = Logic.strip_params goali;
           val ts = find_subterms t 0 [];
-          val ts' = filter eq_terms ts;
-          val ts'' = filter (is_chfin sign T params) ts';
-          val thms = foldl (prove_cont tac sign s T prems params) ([], ts'');
+          val ts' = List.filter eq_terms ts;
+          val ts'' = List.filter (is_chfin sign T params) ts';
+          val thms = Library.foldl (prove_cont tac sign s T prems params) ([], ts'');
         in
           (case thms of
             ((ts as ((t', _)::_), cont_thm)::_) =>
               let
                 val paths = map snd ts;