src/HOL/Tools/refute.ML
changeset 42364 8c674b3b8e44
parent 42361 23f352990944
child 42680 b6c27cf04fe9
     1.1 --- a/src/HOL/Tools/refute.ML	Sat Apr 16 16:37:21 2011 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Sat Apr 16 18:11:20 2011 +0200
     1.3 @@ -1628,7 +1628,7 @@
     1.4            Const (_, T) => interpret_groundterm T
     1.5          | Free (_, T) => interpret_groundterm T
     1.6          | Var (_, T) => interpret_groundterm T
     1.7 -        | Bound i => SOME (List.nth (#bounds args, i), model, args)
     1.8 +        | Bound i => SOME (nth (#bounds args) i, model, args)
     1.9          | Abs (x, T, body) =>
    1.10              let
    1.11                (* create all constants of type 'T' *)
    1.12 @@ -2271,7 +2271,7 @@
    1.13                          else ()
    1.14                        (* the type of a recursion operator is *)
    1.15                        (* [T1, ..., Tn, IDT] ---> Tresult     *)
    1.16 -                      val IDT = List.nth (binder_types T, mconstrs_count)
    1.17 +                      val IDT = nth (binder_types T) mconstrs_count
    1.18                        (* by our assumption on the order of recursion operators *)
    1.19                        (* and datatypes, this is the index of the datatype      *)
    1.20                        (* corresponding to the given recursion operator         *)
    1.21 @@ -2463,15 +2463,15 @@
    1.22                                (* find the indices of the constructor's /recursive/ *)
    1.23                                (* arguments                                         *)
    1.24                                val (_, _, constrs) = the (AList.lookup (op =) descr idx)
    1.25 -                              val (_, dtyps)      = List.nth (constrs, c)
    1.26 -                              val rec_dtyps_args  = filter
    1.27 +                              val (_, dtyps) = nth constrs c
    1.28 +                              val rec_dtyps_args = filter
    1.29                                  (Datatype_Aux.is_rec_type o fst) (dtyps ~~ args)
    1.30                                (* map those indices to interpretations *)
    1.31                                val rec_dtyps_intrs = map (fn (dtyp, arg) =>
    1.32                                  let
    1.33 -                                  val dT     = typ_of_dtyp descr typ_assoc dtyp
    1.34 +                                  val dT = typ_of_dtyp descr typ_assoc dtyp
    1.35                                    val consts = make_constants ctxt (typs, []) dT
    1.36 -                                  val arg_i  = List.nth (consts, arg)
    1.37 +                                  val arg_i = nth consts arg
    1.38                                  in
    1.39                                    (dtyp, arg_i)
    1.40                                  end) rec_dtyps_args
    1.41 @@ -3104,7 +3104,7 @@
    1.42                        (* generate all constants                                 *)
    1.43                        val consts = make_constants ctxt (typs, []) dT
    1.44                      in
    1.45 -                      print ctxt (typs, []) dT (List.nth (consts, n)) assignment
    1.46 +                      print ctxt (typs, []) dT (nth consts n) assignment
    1.47                      end) (cargs ~~ args)
    1.48                  in
    1.49                    SOME (list_comb (cTerm, argsTerms))