src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 39345 062c10ff848c
parent 39118 12f3788be67b
child 39359 6f49c7fbb1b1
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Sep 13 20:21:24 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Sep 13 20:21:40 2010 +0200
     1.3 @@ -904,18 +904,6 @@
     1.4      fun term_for_rep maybe_opt unfold =
     1.5        reconstruct_term maybe_opt unfold pool wacky_names scope atomss
     1.6                         sel_names rel_table bounds
     1.7 -    fun nth_value_of_type card T n =
     1.8 -      let
     1.9 -        fun aux unfold = term_for_rep true unfold T T (Atom (card, 0)) [[n]]
    1.10 -      in
    1.11 -        case aux false of
    1.12 -          t as Const (s, _) =>
    1.13 -          if String.isPrefix (cyclic_const_prefix ()) s then
    1.14 -            HOLogic.mk_eq (t, aux true)
    1.15 -          else
    1.16 -            t
    1.17 -        | t => t
    1.18 -      end
    1.19      val all_values =
    1.20        all_values_of_type pool wacky_names scope atomss sel_names rel_table
    1.21                           bounds