src/Pure/IsaPlanner/term_lib.ML

           handle Type.TUNIFY => NONE;
     in
       case typs_unify of
         SOME (typinsttab, ix2) =>
         let 
-      (* is it right to throw away teh flexes? 
+      (* is it right to throw away the flexes? 
          or should I be using them somehow? *)
           fun mk_insts (env,flexflexes) = 
               (Vartab.dest (Envir.type_env env),  Envir.alist_of env);
           val initenv = Envir.Envir {asol = Vartab.empty, 
                                      iTs = typinsttab, maxidx = ix2};
           val useq = (Unify.unifiers (sgn,initenv,[a]))
-              handle Library.LIST _ => Seq.empty
-                   | Term.TERM _ => Seq.empty;
+	      handle UnequalLengths => Seq.empty
+		   | Term.TERM _ => Seq.empty;
           fun clean_unify' useq () = 
               (case (Seq.pull useq) of 
                  NONE => NONE
                | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
-              handle Library.LIST _ => NONE
+	      handle UnequalLengths => NONE
                    | Term.TERM _ => NONE;
         in
           (Seq.make (clean_unify' useq))
         end
       | NONE => Seq.empty

     val unskolemise_term : (string,Term.typ) list -> Term.term -> Term.term
 *)
 
 (* cunning version *)
 
-(* This version avoids name conflicts that might be intorduced by
+(* This version avoids name conflicts that might be introduced by
 unskolemisation, and returns a list of (string * Term.typ) * string,
 where the outer string is the original name, and the inner string is
 the new name, and the type is the type of the free variable that was
 renamed. *)
 local

           let val renamedn = Term.variant names n' in 
             (renamedn, (((renamedn, ty), n) :: renames, 
                         renamedn :: names)) end
         | (SOME ((renamedn, _), _)) => (renamedn, L)
       end
-      handle LIST _ => (n, L);
+      handle Fail _ => (n, L);
 
   fun unsk (L,f) (t1 $ t2) = 
       let val (L', t1') = unsk (L, I) t1 
       in unsk (L', (fn x => f (t1' $ x))) t2 end
     | unsk (L,f) (Abs(n,ty,t)) = 

         let 
           fun fmap fv = 
               let (n,ty) = (Term.dest_Free fv) in 
                 SOME (fv, Free (Syntax.dest_skolem n, ty)) handle LIST _ => NONE
               end
-          val substfrees = mapfilter fmap (Term.term_frees t)
+          val substfrees = List.mapPartial fmap (Term.term_frees t)
         in
           Term.subst_free substfrees t
         end; *)
 
 (* true if the type t is a function *)

 
 val is_atomic_typ = not o is_fun_typ;
 
 (* get the frees in a term that are of atomic type, ie non-functions *)
 val atomic_frees_of_term =
-     filter (is_atomic_typ o snd) 
+     List.filter (is_atomic_typ o snd) 
      o map Term.dest_Free 
      o Term.term_frees;
 
 
 (* read in a string and a top-level type and this will give back a term *) 

 
   | term_name_eq (ah $ at) (bh $ bt) l =
     let 
       val lopt = (term_name_eq ah bh l)
     in
-      if is_some lopt then 
-	term_name_eq at bt (the lopt)
+      if isSome lopt then 
+	term_name_eq at bt (valOf lopt)
       else
         NONE
     end
 
   | term_name_eq (Const(a,T)) (Const(b,U)) l = 

   | term_name_eq a b l = ((*writeln ("unchecked case:\n" ^ "a:\n" ^ (pretty_print_term a) ^ "\nb:\n" ^ (pretty_print_term b));*) NONE);
 
  (* checks to see if the term in a name-equivalent member of the list of terms. *)
   fun get_name_eq_member a [] = NONE
     | get_name_eq_member a (h :: t) = 
-        if is_some (term_name_eq a h []) then SOME h 
+        if isSome (term_name_eq a h []) then SOME h 
 				else get_name_eq_member a t;
 
   fun name_eq_member a [] = false
     | name_eq_member a (h :: t) = 
-        if is_some (term_name_eq a h []) then true 
+        if isSome (term_name_eq a h []) then true 
 				else name_eq_member a t;
 
   (* true if term is a variable *)
   fun is_some_kind_of_var (Free(s, ty)) = true
     | is_some_kind_of_var (Var(i, ty)) = true

     term_contains1 (NONE::Bs, FVs) t t2
 
   | term_contains1 T (ah $ at) (bh $ bt) =
     (term_contains1 T ah (bh $ bt)) @ 
     (term_contains1 T at (bh $ bt)) @
-    (flat (map (fn inT => (term_contains1 inT at bt)) 
+    (List.concat (map (fn inT => (term_contains1 inT at bt)) 
                (term_contains1 T ah bh)))
 
   | term_contains1 T a (bh $ bt) = []
 
   | term_contains1 T (ah $ at) b =

      (case (fvartabS.lookup (ntab,s)) of
       NONE => ((fvartabS.update ((s,s),ntab)), v)
     | SOME _ => nt)
   | bounds_to_frees_aux T (nt as (ntab, Bound i)) = 
     let 
-      val (s,ty) = Library.nth_elem (i,T) 
+      val (s,ty) = List.nth (T,i) 
     in
       (ntab, Free (s,ty))
     end;
 
 

     Abs(s,ty,loose_bnds_to_frees_aux (bnds + 1,vars) t)
   | loose_bnds_to_frees_aux (bnds,vars) (a $ b) = 
     (loose_bnds_to_frees_aux (bnds,vars) a) 
       $ (loose_bnds_to_frees_aux (bnds,vars) b)
   | loose_bnds_to_frees_aux (bnds,vars) (t as (Bound i)) = 
-    if (bnds <= i) then Free (Library.nth_elem (i - bnds,vars))
+    if (bnds <= i) then Free (List.nth (vars,i - bnds))
     else t
   | loose_bnds_to_frees_aux (bnds,vars) t = t;
 
 
 fun loose_bnds_to_frees vars t = 

       SplitterData.mk_eq (Drule.standard (ObjectLogic.rulify_no_asm triv))
     end;
 
 fun thms_of_prems_in_goal i tm= 
     let 
-      val goal = (nth_elem (i-1,Thm.prems_of tm))
+      val goal = (List.nth (Thm.prems_of tm,i-1))
       val vars = rev (strip_all_vars goal)
       val prems = Logic.strip_assums_hyp (strip_all_body goal)
       val simp_prem_thms = 
 					map (make_term_into_simp_thm vars (Thm.sign_of_thm tm)) prems
     in