src/HOL/Tools/refute.ML

     | NONE =>
         (case t of
           Const (_, T) => interpret_groundterm T
         | Free (_, T) => interpret_groundterm T
         | Var (_, T) => interpret_groundterm T
-        | Bound i => SOME (List.nth (#bounds args, i), model, args)
+        | Bound i => SOME (nth (#bounds args) i, model, args)
         | Abs (x, T, body) =>
             let
               (* create all constants of type 'T' *)
               val constants = make_constants ctxt model T
               (* interpret the 'body' separately for each constant *)

                           raise REFUTE ("IDT_recursion_interpreter",
                             "datatype argument is not a variable")
                         else ()
                       (* the type of a recursion operator is *)
                       (* [T1, ..., Tn, IDT] ---> Tresult     *)
-                      val IDT = List.nth (binder_types T, mconstrs_count)
+                      val IDT = nth (binder_types T) mconstrs_count
                       (* by our assumption on the order of recursion operators *)
                       (* and datatypes, this is the index of the datatype      *)
                       (* corresponding to the given recursion operator         *)
                       val idt_index = find_index (fn s' => s' = s) (#rec_names info)
                       (* mutually recursive types must have the same type   *)

                               (* int * int list *)
                               val (c, args) = get_cargs idx elem
                               (* find the indices of the constructor's /recursive/ *)
                               (* arguments                                         *)
                               val (_, _, constrs) = the (AList.lookup (op =) descr idx)
-                              val (_, dtyps)      = List.nth (constrs, c)
-                              val rec_dtyps_args  = filter
+                              val (_, dtyps) = nth constrs c
+                              val rec_dtyps_args = filter
                                 (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args)
                               (* map those indices to interpretations *)
                               val rec_dtyps_intrs = map (fn (dtyp, arg) =>
                                 let
-                                  val dT     = typ_of_dtyp descr typ_assoc dtyp
+                                  val dT = typ_of_dtyp descr typ_assoc dtyp
                                   val consts = make_constants ctxt (typs, []) dT
-                                  val arg_i  = List.nth (consts, arg)
+                                  val arg_i = nth consts arg
                                 in
                                   (dtyp, arg_i)
                                 end) rec_dtyps_args
                               (* takes the dtyp and interpretation of an element, *)
                               (* and computes the interpretation for the          *)

                       (* we only need the n-th element of this list, so there   *)
                       (* might be a more efficient implementation that does not *)
                       (* generate all constants                                 *)
                       val consts = make_constants ctxt (typs, []) dT
                     in
-                      print ctxt (typs, []) dT (List.nth (consts, n)) assignment
+                      print ctxt (typs, []) dT (nth consts n) assignment
                     end) (cargs ~~ args)
                 in
                   SOME (list_comb (cTerm, argsTerms))
                 end
             end