tuned ML names
authorblanchet
Mon Mar 03 22:33:22 2014 +0100 (2014-03-03 ago)
changeset 55890bd7927cca152
parent 55889 6bfbec3dff62
child 55891 d1a9b07783ab
tuned ML names
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 03 22:33:22 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -378,7 +378,7 @@
     1.4                   ". " ^ extra))
     1.5        end
     1.6      fun is_type_fundamentally_monotonic T =
     1.7 -      (is_datatype ctxt T andalso not (is_quot_type ctxt T) andalso
     1.8 +      (is_data_type ctxt T andalso not (is_quot_type ctxt T) andalso
     1.9         (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
    1.10        is_number_type ctxt T orelse is_bit_type T
    1.11      fun is_type_actually_monotonic T =
    1.12 @@ -395,15 +395,15 @@
    1.13          SOME (SOME b) => b
    1.14        | _ => is_type_fundamentally_monotonic T orelse
    1.15               is_type_actually_monotonic T
    1.16 -    fun is_deep_datatype_finitizable T =
    1.17 +    fun is_deep_data_type_finitizable T =
    1.18        triple_lookup (type_match thy) finitizes T = SOME (SOME true)
    1.19 -    fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
    1.20 +    fun is_shallow_data_type_finitizable (T as Type (@{type_name fun_box}, _)) =
    1.21          is_type_kind_of_monotonic T
    1.22 -      | is_shallow_datatype_finitizable T =
    1.23 +      | is_shallow_data_type_finitizable T =
    1.24          case triple_lookup (type_match thy) finitizes T of
    1.25            SOME (SOME b) => b
    1.26          | _ => is_type_kind_of_monotonic T
    1.27 -    fun is_datatype_deep T =
    1.28 +    fun is_data_type_deep T =
    1.29        T = @{typ unit} orelse T = nat_T orelse is_word_type T orelse
    1.30        exists (curry (op =) T o domain_type o type_of) sel_names
    1.31      val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
    1.32 @@ -438,13 +438,13 @@
    1.33        else
    1.34          ()
    1.35      val (deep_dataTs, shallow_dataTs) =
    1.36 -      all_Ts |> filter (is_datatype ctxt)
    1.37 -             |> List.partition is_datatype_deep
    1.38 +      all_Ts |> filter (is_data_type ctxt)
    1.39 +             |> List.partition is_data_type_deep
    1.40      val finitizable_dataTs =
    1.41        (deep_dataTs |> filter_out (is_finite_type hol_ctxt)
    1.42 -                   |> filter is_deep_datatype_finitizable) @
    1.43 +                   |> filter is_deep_data_type_finitizable) @
    1.44        (shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
    1.45 -                      |> filter is_shallow_datatype_finitizable)
    1.46 +                      |> filter is_shallow_data_type_finitizable)
    1.47      val _ =
    1.48        if verbose andalso not (null finitizable_dataTs) then
    1.49          pprint_v (K (monotonicity_message finitizable_dataTs
    1.50 @@ -484,7 +484,7 @@
    1.51      val too_big_scopes = Unsynchronized.ref []
    1.52  
    1.53      fun problem_for_scope unsound
    1.54 -            (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
    1.55 +            (scope as {card_assigns, bits, bisim_depth, data_types, ofs, ...}) =
    1.56        let
    1.57          val _ = not (exists (fn other => scope_less_eq other scope)
    1.58                              (!too_big_scopes)) orelse
    1.59 @@ -500,7 +500,7 @@
    1.60          val effective_total_consts =
    1.61            case total_consts of
    1.62              SOME b => b
    1.63 -          | NONE => forall (is_exact_type datatypes true) all_Ts
    1.64 +          | NONE => forall (is_exact_type data_types true) all_Ts
    1.65          val main_j0 = offset_of_type ofs bool_T
    1.66          val (nat_card, nat_j0) = spec_of_type scope nat_T
    1.67          val (int_card, int_j0) = spec_of_type scope int_T
    1.68 @@ -569,12 +569,13 @@
    1.69          val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
    1.70          val need_vals =
    1.71            map (fn dtype as {typ, ...} =>
    1.72 -                  (typ, needed_values_for_datatype need_us ofs dtype)) datatypes
    1.73 +                  (typ, needed_values_for_data_type need_us ofs dtype))
    1.74 +              data_types
    1.75          val sel_bounds =
    1.76 -          map (bound_for_sel_rel ctxt debug need_vals datatypes) sel_rels
    1.77 +          map (bound_for_sel_rel ctxt debug need_vals data_types) sel_rels
    1.78          val dtype_axioms =
    1.79 -          declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
    1.80 -              datatype_sym_break bits ofs kk rel_table datatypes
    1.81 +          declarative_axioms_for_data_types hol_ctxt binarize need_us need_vals
    1.82 +              datatype_sym_break bits ofs kk rel_table data_types
    1.83          val declarative_axioms = plain_axioms @ dtype_axioms
    1.84          val univ_card = Int.max (univ_card nat_card int_card main_j0
    1.85                                       (plain_bounds @ sel_bounds) formula,
    1.86 @@ -607,7 +608,7 @@
    1.87                 problem_for_scope unsound
    1.88                     {hol_ctxt = hol_ctxt, binarize = binarize,
    1.89                      card_assigns = card_assigns, bits = bits,
    1.90 -                    bisim_depth = bisim_depth, datatypes = datatypes,
    1.91 +                    bisim_depth = bisim_depth, data_types = data_types,
    1.92                      ofs = Typtab.empty}
    1.93               else if loc = "Nitpick.pick_them_nits_in_term.\
    1.94                             \problem_for_scope" then
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 22:33:22 2014 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Mar 03 22:33:22 2014 +0100
     2.3 @@ -115,7 +115,7 @@
     2.4    val is_quot_type : Proof.context -> typ -> bool
     2.5    val is_pure_typedef : Proof.context -> typ -> bool
     2.6    val is_univ_typedef : Proof.context -> typ -> bool
     2.7 -  val is_datatype : Proof.context -> typ -> bool
     2.8 +  val is_data_type : Proof.context -> typ -> bool
     2.9    val is_record_constr : string * typ -> bool
    2.10    val is_record_get : theory -> string * typ -> bool
    2.11    val is_record_update : theory -> string * typ -> bool
    2.12 @@ -160,10 +160,10 @@
    2.13    val unregister_codatatype :
    2.14      typ -> morphism -> Context.generic -> Context.generic
    2.15    val unregister_codatatype_global : typ -> theory -> theory
    2.16 -  val datatype_constrs : hol_context -> typ -> (string * typ) list
    2.17 -  val binarized_and_boxed_datatype_constrs :
    2.18 +  val data_type_constrs : hol_context -> typ -> (string * typ) list
    2.19 +  val binarized_and_boxed_data_type_constrs :
    2.20      hol_context -> bool -> typ -> (string * typ) list
    2.21 -  val num_datatype_constrs : hol_context -> typ -> int
    2.22 +  val num_data_type_constrs : hol_context -> typ -> int
    2.23    val constr_name_for_sel_like : string -> string
    2.24    val binarized_and_boxed_constr_for_sel : hol_context -> bool ->
    2.25      string * typ -> string * typ
    2.26 @@ -613,9 +613,7 @@
    2.27  val is_raw_typedef = is_some oo typedef_info
    2.28  val is_raw_old_datatype = is_some oo Datatype.get_info
    2.29  
    2.30 -(* FIXME: Use antiquotation for "natural" below or detect "rep_datatype",
    2.31 -   e.g., by adding a field to "Datatype_Aux.info". *)
    2.32 -val is_basic_datatype =
    2.33 +val is_interpreted_type =
    2.34    member (op =) [@{type_name prod}, @{type_name set}, @{type_name bool},
    2.35                   @{type_name nat}, @{type_name int}, @{type_name natural},
    2.36                   @{type_name integer}]
    2.37 @@ -665,7 +663,7 @@
    2.38      val (co_s, coTs) = dest_Type coT
    2.39      val _ =
    2.40        if forall is_TFree coTs andalso not (has_duplicates (op =) coTs) andalso
    2.41 -         co_s <> @{type_name fun} andalso not (is_basic_datatype co_s) then
    2.42 +         co_s <> @{type_name fun} andalso not (is_interpreted_type co_s) then
    2.43          ()
    2.44        else
    2.45          raise TYPE ("Nitpick_HOL.register_codatatype_generic", [coT], [])
    2.46 @@ -744,11 +742,11 @@
    2.47       | NONE => false)
    2.48    | is_univ_typedef _ _ = false
    2.49  
    2.50 -fun is_datatype ctxt (T as Type (s, _)) =
    2.51 +fun is_data_type ctxt (T as Type (s, _)) =
    2.52      (is_raw_typedef ctxt s orelse is_registered_type ctxt T orelse
    2.53       T = @{typ ind} orelse is_raw_quot_type ctxt T) andalso
    2.54 -    not (is_basic_datatype s)
    2.55 -  | is_datatype _ _ = false
    2.56 +    not (is_interpreted_type s)
    2.57 +  | is_data_type _ _ = false
    2.58  
    2.59  fun all_record_fields thy T =
    2.60    let val (recs, more) = Record.get_extT_fields thy T in
    2.61 @@ -891,7 +889,7 @@
    2.62  
    2.63  fun is_constr ctxt (x as (_, T)) =
    2.64    is_nonfree_constr ctxt x andalso
    2.65 -  not (is_basic_datatype (fst (dest_Type (unarize_type (body_type T))))) andalso
    2.66 +  not (is_interpreted_type (fst (dest_Type (unarize_type (body_type T))))) andalso
    2.67    not (is_stale_constr ctxt x)
    2.68  
    2.69  val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
    2.70 @@ -1000,8 +998,8 @@
    2.71  fun zero_const T = Const (@{const_name zero_class.zero}, T)
    2.72  fun suc_const T = Const (@{const_name Suc}, T --> T)
    2.73  
    2.74 -fun uncached_datatype_constrs ({thy, ctxt, ...} : hol_context)
    2.75 -                              (T as Type (s, Ts)) =
    2.76 +fun uncached_data_type_constrs ({thy, ctxt, ...} : hol_context)
    2.77 +                               (T as Type (s, Ts)) =
    2.78      (case AList.lookup (op =) (#codatatypes (Data.get (Context.Proof ctxt)))
    2.79                         s of
    2.80         SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type T)) xs'
    2.81 @@ -1017,7 +1015,7 @@
    2.82                [(Abs_name,
    2.83                  varify_and_instantiate_type ctxt abs_type T rep_type --> T)]
    2.84              | NONE => [] (* impossible *)
    2.85 -          else if is_datatype ctxt T then
    2.86 +          else if is_data_type ctxt T then
    2.87              case Datatype.get_info thy s of
    2.88                SOME {index, descr, ...} =>
    2.89                let
    2.90 @@ -1047,20 +1045,20 @@
    2.91                    []
    2.92            else
    2.93              []))
    2.94 -  | uncached_datatype_constrs _ _ = []
    2.95 +  | uncached_data_type_constrs _ _ = []
    2.96  
    2.97 -fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
    2.98 +fun data_type_constrs (hol_ctxt as {constr_cache, ...}) T =
    2.99    case AList.lookup (op =) (!constr_cache) T of
   2.100      SOME xs => xs
   2.101    | NONE =>
   2.102 -    let val xs = uncached_datatype_constrs hol_ctxt T in
   2.103 +    let val xs = uncached_data_type_constrs hol_ctxt T in
   2.104        (Unsynchronized.change constr_cache (cons (T, xs)); xs)
   2.105      end
   2.106  
   2.107 -fun binarized_and_boxed_datatype_constrs hol_ctxt binarize =
   2.108 +fun binarized_and_boxed_data_type_constrs hol_ctxt binarize =
   2.109    map (apsnd ((binarize ? binarize_nat_and_int_in_type)
   2.110 -              o box_type hol_ctxt InConstr)) o datatype_constrs hol_ctxt
   2.111 -val num_datatype_constrs = length oo datatype_constrs
   2.112 +              o box_type hol_ctxt InConstr)) o data_type_constrs hol_ctxt
   2.113 +val num_data_type_constrs = length oo data_type_constrs
   2.114  
   2.115  fun constr_name_for_sel_like @{const_name fst} = @{const_name Pair}
   2.116    | constr_name_for_sel_like @{const_name snd} = @{const_name Pair}
   2.117 @@ -1069,7 +1067,7 @@
   2.118  fun binarized_and_boxed_constr_for_sel hol_ctxt binarize (s', T') =
   2.119    let val s = constr_name_for_sel_like s' in
   2.120      AList.lookup (op =)
   2.121 -        (binarized_and_boxed_datatype_constrs hol_ctxt binarize (domain_type T'))
   2.122 +        (binarized_and_boxed_data_type_constrs hol_ctxt binarize (domain_type T'))
   2.123          s
   2.124      |> the |> pair s
   2.125    end
   2.126 @@ -1146,7 +1144,7 @@
   2.127         | @{typ prop} => 2
   2.128         | @{typ bool} => 2
   2.129         | Type _ =>
   2.130 -         (case datatype_constrs hol_ctxt T of
   2.131 +         (case data_type_constrs hol_ctxt T of
   2.132              [] => if is_integer_type T orelse is_bit_type T then 0
   2.133                    else raise SAME ()
   2.134            | constrs =>
   2.135 @@ -1243,7 +1241,7 @@
   2.136      if s = @{const_name Suc} then
   2.137        Abs (Name.uu, dataT,
   2.138             @{const Not} $ HOLogic.mk_eq (zero_const dataT, Bound 0))
   2.139 -    else if num_datatype_constrs hol_ctxt dataT >= 2 then
   2.140 +    else if num_data_type_constrs hol_ctxt dataT >= 2 then
   2.141        Const (discr_for_constr x)
   2.142      else
   2.143        Abs (Name.uu, dataT, @{const True})
   2.144 @@ -1317,7 +1315,7 @@
   2.145                   (@{const_name Pair}, T1 --> T2 --> T)
   2.146                 end
   2.147               else
   2.148 -               datatype_constrs hol_ctxt T |> hd
   2.149 +               data_type_constrs hol_ctxt T |> hd
   2.150             val arg_Ts = binder_types T'
   2.151           in
   2.152             list_comb (Const x', map2 (select_nth_constr_arg ctxt x' t)
   2.153 @@ -1383,7 +1381,6 @@
   2.154  fun special_bounds ts =
   2.155    fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
   2.156  
   2.157 -(* FIXME: detect "rep_datatype"? *)
   2.158  fun is_funky_typedef_name ctxt s =
   2.159    member (op =) [@{type_name unit}, @{type_name prod}, @{type_name set},
   2.160                   @{type_name Sum_Type.sum}, @{type_name int}] s orelse
   2.161 @@ -1529,7 +1526,7 @@
   2.162  fun case_const_names ctxt =
   2.163    let val thy = Proof_Context.theory_of ctxt in
   2.164      Symtab.fold (fn (dtype_s, {index, descr, case_name, ...}) =>
   2.165 -                    if is_basic_datatype dtype_s then
   2.166 +                    if is_interpreted_type dtype_s then
   2.167                        I
   2.168                      else
   2.169                        cons (case_name, AList.lookup (op =) descr index
   2.170 @@ -1668,7 +1665,7 @@
   2.171  
   2.172  fun optimized_case_def (hol_ctxt as {ctxt, ...}) Ts dataT res_T func_ts =
   2.173    let
   2.174 -    val xs = datatype_constrs hol_ctxt dataT
   2.175 +    val xs = data_type_constrs hol_ctxt dataT
   2.176      val cases =
   2.177        func_ts ~~ xs
   2.178        |> map (fn (func_t, x) =>
   2.179 @@ -1695,7 +1692,7 @@
   2.180    |> absdummy dataT
   2.181  
   2.182  fun optimized_record_get (hol_ctxt as {thy, ctxt, ...}) s rec_T res_T t =
   2.183 -  let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in
   2.184 +  let val constr_x = hd (data_type_constrs hol_ctxt rec_T) in
   2.185      case no_of_record_field thy s rec_T of
   2.186        ~1 => (case rec_T of
   2.187                 Type (_, Ts as _ :: _) =>
   2.188 @@ -1714,7 +1711,7 @@
   2.189  fun optimized_record_update (hol_ctxt as {thy, ctxt, ...}) s rec_T fun_t
   2.190                              rec_t =
   2.191    let
   2.192 -    val constr_x as (_, constr_T) = hd (datatype_constrs hol_ctxt rec_T)
   2.193 +    val constr_x as (_, constr_T) = hd (data_type_constrs hol_ctxt rec_T)
   2.194      val Ts = binder_types constr_T
   2.195      val n = length Ts
   2.196      val special_j = no_of_record_field thy s rec_T
   2.197 @@ -1858,7 +1855,7 @@
   2.198                else if is_quot_abs_fun ctxt x then
   2.199                  case T of
   2.200                    Type (@{type_name fun}, [rep_T, abs_T as Type (abs_s, _)]) =>
   2.201 -                  if is_basic_datatype abs_s then
   2.202 +                  if is_interpreted_type abs_s then
   2.203                      raise NOT_SUPPORTED ("abstraction function on " ^
   2.204                                           quote abs_s)
   2.205                    else
   2.206 @@ -1869,7 +1866,7 @@
   2.207                else if is_quot_rep_fun ctxt x then
   2.208                  case T of
   2.209                    Type (@{type_name fun}, [abs_T as Type (abs_s, _), rep_T]) =>
   2.210 -                  if is_basic_datatype abs_s then
   2.211 +                  if is_interpreted_type abs_s then
   2.212                      raise NOT_SUPPORTED ("representation function on " ^
   2.213                                           quote abs_s)
   2.214                    else
   2.215 @@ -2109,7 +2106,7 @@
   2.216  
   2.217  fun codatatype_bisim_axioms (hol_ctxt as {ctxt, ...}) T =
   2.218    let
   2.219 -    val xs = datatype_constrs hol_ctxt T
   2.220 +    val xs = data_type_constrs hol_ctxt T
   2.221      val pred_T = T --> bool_T
   2.222      val iter_T = @{typ bisim_iterator}
   2.223      val bisim_max = @{const bisim_iterator_max}
   2.224 @@ -2495,8 +2492,8 @@
   2.225            accum
   2.226          else
   2.227            T :: accum
   2.228 -          |> fold aux (case binarized_and_boxed_datatype_constrs hol_ctxt
   2.229 -                                                                 binarize T of
   2.230 +          |> fold aux (case binarized_and_boxed_data_type_constrs hol_ctxt
   2.231 +                                                                  binarize T of
   2.232                           [] => Ts
   2.233                         | xs => map snd xs)
   2.234        | _ => insert (op =) T accum
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 03 22:33:22 2014 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Mar 03 22:33:22 2014 +0100
     3.3 @@ -8,7 +8,7 @@
     3.4  signature NITPICK_KODKOD =
     3.5  sig
     3.6    type hol_context = Nitpick_HOL.hol_context
     3.7 -  type datatype_spec = Nitpick_Scope.datatype_spec
     3.8 +  type data_type_spec = Nitpick_Scope.data_type_spec
     3.9    type kodkod_constrs = Nitpick_Peephole.kodkod_constrs
    3.10    type nut = Nitpick_Nut.nut
    3.11  
    3.12 @@ -28,17 +28,17 @@
    3.13    val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
    3.14    val bound_for_sel_rel :
    3.15      Proof.context -> bool -> (typ * (nut * int) list option) list
    3.16 -    -> datatype_spec list -> nut -> Kodkod.bound
    3.17 +    -> data_type_spec list -> nut -> Kodkod.bound
    3.18    val merge_bounds : Kodkod.bound list -> Kodkod.bound list
    3.19    val kodkod_formula_from_nut :
    3.20      int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
    3.21 -  val needed_values_for_datatype :
    3.22 -    nut list -> int Typtab.table -> datatype_spec -> (nut * int) list option
    3.23 +  val needed_values_for_data_type :
    3.24 +    nut list -> int Typtab.table -> data_type_spec -> (nut * int) list option
    3.25    val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
    3.26 -  val declarative_axioms_for_datatypes :
    3.27 +  val declarative_axioms_for_data_types :
    3.28      hol_context -> bool -> nut list -> (typ * (nut * int) list option) list
    3.29      -> int -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
    3.30 -    -> datatype_spec list -> Kodkod.formula list
    3.31 +    -> data_type_spec list -> Kodkod.formula list
    3.32  end;
    3.33  
    3.34  structure Nitpick_Kodkod : NITPICK_KODKOD =
    3.35 @@ -55,8 +55,8 @@
    3.36  
    3.37  fun pull x xs = x :: filter_out (curry (op =) x) xs
    3.38  
    3.39 -fun is_datatype_acyclic ({co = false, deep = true, ...} : datatype_spec) = true
    3.40 -  | is_datatype_acyclic _ = false
    3.41 +fun is_data_type_acyclic ({co = false, deep = true, ...} : data_type_spec) = true
    3.42 +  | is_data_type_acyclic _ = false
    3.43  
    3.44  fun flip_nums n = index_seq 1 n @ [0] |> map KK.Num
    3.45  
    3.46 @@ -317,7 +317,7 @@
    3.47    | bound_for_plain_rel _ _ u =
    3.48      raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
    3.49  
    3.50 -fun is_datatype_nat_like ({typ, constrs, ...} : datatype_spec) =
    3.51 +fun is_data_type_nat_like ({typ, constrs, ...} : data_type_spec) =
    3.52    case constrs of
    3.53      [_, _] =>
    3.54      (case constrs |> map (snd o #const) |> List.partition is_fun_type of
    3.55 @@ -328,7 +328,7 @@
    3.56  fun needed_values need_vals T =
    3.57    AList.lookup (op =) need_vals T |> the_default NONE |> these
    3.58  
    3.59 -fun all_values_are_needed need_vals ({typ, card, ...} : datatype_spec) =
    3.60 +fun all_values_are_needed need_vals ({typ, card, ...} : data_type_spec) =
    3.61    length (needed_values need_vals typ) = card
    3.62  
    3.63  fun is_sel_of_constr x (Construct (sel_us, _, _, _), _) =
    3.64 @@ -342,7 +342,7 @@
    3.65        val constr_s = original_name nick
    3.66        val {delta, epsilon, exclusive, explicit_max, ...} =
    3.67          constr_spec dtypes (constr_s, T1)
    3.68 -      val dtype as {card, ...} = datatype_spec dtypes T1 |> the
    3.69 +      val dtype as {card, ...} = data_type_spec dtypes T1 |> the
    3.70        val T1_need_vals = needed_values need_vals T1
    3.71      in
    3.72        ([(x, bound_comment ctxt debug nick T R)],
    3.73 @@ -352,7 +352,7 @@
    3.74           val (my_need_vals, other_need_vals) =
    3.75             T1_need_vals |> List.partition (is_sel_of_constr x)
    3.76           fun atom_seq_for_self_rec j =
    3.77 -           if is_datatype_nat_like dtype then (1, j + j0 - 1) else (j, j0)
    3.78 +           if is_data_type_nat_like dtype then (1, j + j0 - 1) else (j, j0)
    3.79           fun exact_bound_for_perhaps_needy_atom j =
    3.80             case AList.find (op =) my_need_vals j of
    3.81               [constr_u] =>
    3.82 @@ -408,7 +408,7 @@
    3.83             else
    3.84               [bound_tuples false,
    3.85                if T1 = T2 andalso epsilon > delta andalso
    3.86 -                 is_datatype_acyclic dtype then
    3.87 +                 is_data_type_acyclic dtype then
    3.88                  index_seq delta (epsilon - delta)
    3.89                  |> map (fn j => tuple_product (KK.TupleSet [KK.Tuple [j + j0]])
    3.90                                      (KK.TupleAtomSeq (atom_seq_for_self_rec j)))
    3.91 @@ -1502,7 +1502,7 @@
    3.92  
    3.93  fun nfa_transitions_for_sel hol_ctxt binarize
    3.94                              ({kk_project, ...} : kodkod_constrs) rel_table
    3.95 -                            (dtypes : datatype_spec list) constr_x n =
    3.96 +                            (dtypes : data_type_spec list) constr_x n =
    3.97    let
    3.98      val x as (_, T) =
    3.99        binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize constr_x n
   3.100 @@ -1520,10 +1520,10 @@
   3.101    maps (nfa_transitions_for_sel hol_ctxt binarize kk rel_table dtypes x)
   3.102         (index_seq 0 (num_sels_for_constr_type T))
   3.103  
   3.104 -fun nfa_entry_for_datatype _ _ _ _ _ ({co = true, ...} : datatype_spec) = NONE
   3.105 -  | nfa_entry_for_datatype _ _ _ _ _ {deep = false, ...} = NONE
   3.106 -  | nfa_entry_for_datatype hol_ctxt binarize kk rel_table dtypes
   3.107 -                           {typ, constrs, ...} =
   3.108 +fun nfa_entry_for_data_type _ _ _ _ _ ({co = true, ...} : data_type_spec) = NONE
   3.109 +  | nfa_entry_for_data_type _ _ _ _ _ {deep = false, ...} = NONE
   3.110 +  | nfa_entry_for_data_type hol_ctxt binarize kk rel_table dtypes
   3.111 +                            {typ, constrs, ...} =
   3.112      SOME (typ, maps (nfa_transitions_for_constr hol_ctxt binarize kk rel_table
   3.113                                                  dtypes o #const) constrs)
   3.114  
   3.115 @@ -1566,17 +1566,17 @@
   3.116    |> Typ_Graph.strong_conn
   3.117    |> map (fn keys => filter (member (op =) keys o fst) nfa)
   3.118  
   3.119 -(* Cycle breaking in the bounds takes care of singly recursive datatypes, hence
   3.120 +(* Cycle breaking in the bounds takes care of singly recursive data types, hence
   3.121     the first equation. *)
   3.122 -fun acyclicity_axioms_for_datatype _ [_] _ = []
   3.123 -  | acyclicity_axioms_for_datatype (kk as {kk_no, kk_intersect, ...}) nfa
   3.124 -                                   start_T =
   3.125 +fun acyclicity_axioms_for_data_type _ [_] _ = []
   3.126 +  | acyclicity_axioms_for_data_type (kk as {kk_no, kk_intersect, ...}) nfa
   3.127 +                                    start_T =
   3.128      [kk_no (kk_intersect
   3.129                  (loop_path_rel_expr kk nfa (pull start_T (map fst nfa)) start_T)
   3.130                  KK.Iden)]
   3.131  
   3.132 -fun acyclicity_axioms_for_datatypes kk =
   3.133 -  maps (fn nfa => maps (acyclicity_axioms_for_datatype kk nfa o fst) nfa)
   3.134 +fun acyclicity_axioms_for_data_types kk =
   3.135 +  maps (fn nfa => maps (acyclicity_axioms_for_data_type kk nfa o fst) nfa)
   3.136  
   3.137  fun atom_equation_for_nut ofs kk (u, j) =
   3.138    let val dummy_u = RelReg (0, type_of u, rep_of u) in
   3.139 @@ -1587,9 +1587,9 @@
   3.140                        "malformed Kodkod formula")
   3.141    end
   3.142  
   3.143 -fun needed_values_for_datatype [] _ _ = SOME []
   3.144 -  | needed_values_for_datatype need_us ofs
   3.145 -                               ({typ, card, constrs, ...} : datatype_spec) =
   3.146 +fun needed_values_for_data_type [] _ _ = SOME []
   3.147 +  | needed_values_for_data_type need_us ofs
   3.148 +                                ({typ, card, constrs, ...} : data_type_spec) =
   3.149      let
   3.150        fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
   3.151            fold aux us
   3.152 @@ -1620,9 +1620,9 @@
   3.153        SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map (rev o snd)
   3.154      end
   3.155  
   3.156 -fun needed_value_axioms_for_datatype _ _ _ (_, NONE) = [KK.False]
   3.157 -  | needed_value_axioms_for_datatype ofs kk dtypes (T, SOME fixed) =
   3.158 -    if is_datatype_nat_like (the (datatype_spec dtypes T)) then []
   3.159 +fun needed_value_axioms_for_data_type _ _ _ (_, NONE) = [KK.False]
   3.160 +  | needed_value_axioms_for_data_type ofs kk dtypes (T, SOME fixed) =
   3.161 +    if is_data_type_nat_like (the (data_type_spec dtypes T)) then []
   3.162      else fixed |> map_filter (atom_equation_for_nut ofs kk)
   3.163  
   3.164  fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
   3.165 @@ -1637,19 +1637,19 @@
   3.166    prod_ord int_ord (prod_ord int_ord (prod_ord int_ord string_ord))
   3.167    o pairself constr_quadruple
   3.168  
   3.169 -fun datatype_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
   3.170 -                   {card = card2, self_rec = self_rec2, constrs = constr2, ...})
   3.171 -                  : datatype_spec * datatype_spec) =
   3.172 +fun data_type_ord (({card = card1, self_rec = self_rec1, constrs = constr1, ...},
   3.173 +                    {card = card2, self_rec = self_rec2, constrs = constr2, ...})
   3.174 +                   : data_type_spec * data_type_spec) =
   3.175    prod_ord int_ord (prod_ord bool_ord int_ord)
   3.176             ((card1, (self_rec1, length constr1)),
   3.177              (card2, (self_rec2, length constr2)))
   3.178  
   3.179 -(* We must absolutely tabulate "suc" for all datatypes whose selector bounds
   3.180 +(* We must absolutely tabulate "suc" for all data types whose selector bounds
   3.181     break cycles; otherwise, we may end up with two incompatible symmetry
   3.182     breaking orders, leading to spurious models. *)
   3.183  fun should_tabulate_suc_for_type dtypes T =
   3.184 -  is_asymmetric_nondatatype T orelse
   3.185 -  case datatype_spec dtypes T of
   3.186 +  is_asymmetric_non_data_type T orelse
   3.187 +  case data_type_spec dtypes T of
   3.188      SOME {self_rec, ...} => self_rec
   3.189    | NONE => false
   3.190  
   3.191 @@ -1673,7 +1673,7 @@
   3.192    | _ :: sel_quadruples' => lex_order_rel_expr kk dtypes sel_quadruples'
   3.193  
   3.194  fun is_nil_like_constr_type dtypes T =
   3.195 -  case datatype_spec dtypes T of
   3.196 +  case data_type_spec dtypes T of
   3.197      SOME {constrs, ...} =>
   3.198      (case filter_out (is_self_recursive_constr_type o snd o #const) constrs of
   3.199         [{const = (_, T'), ...}] => T = T'
   3.200 @@ -1752,8 +1752,8 @@
   3.201        end
   3.202    end
   3.203  
   3.204 -fun sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes
   3.205 -                                  ({constrs, ...} : datatype_spec) =
   3.206 +fun sym_break_axioms_for_data_type hol_ctxt binarize kk rel_table nfas dtypes
   3.207 +                                   ({constrs, ...} : data_type_spec) =
   3.208    let
   3.209      val constrs = sort constr_ord constrs
   3.210      val constr_pairs = all_distinct_unordered_pairs_of constrs
   3.211 @@ -1765,18 +1765,18 @@
   3.212                                                nfas dtypes)
   3.213    end
   3.214  
   3.215 -fun is_datatype_in_needed_value T (Construct (_, T', _, us)) =
   3.216 -    T = T' orelse exists (is_datatype_in_needed_value T) us
   3.217 -  | is_datatype_in_needed_value _ _ = false
   3.218 +fun is_data_type_in_needed_value T (Construct (_, T', _, us)) =
   3.219 +    T = T' orelse exists (is_data_type_in_needed_value T) us
   3.220 +  | is_data_type_in_needed_value _ _ = false
   3.221  
   3.222  val min_sym_break_card = 7
   3.223  
   3.224 -fun sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
   3.225 -                                   kk rel_table nfas dtypes =
   3.226 +fun sym_break_axioms_for_data_types hol_ctxt binarize need_us
   3.227 +      datatype_sym_break kk rel_table nfas dtypes =
   3.228    if datatype_sym_break = 0 then
   3.229      []
   3.230    else
   3.231 -    dtypes |> filter is_datatype_acyclic
   3.232 +    dtypes |> filter is_data_type_acyclic
   3.233             |> filter (fn {constrs = [_], ...} => false
   3.234                         | {card, constrs, ...} =>
   3.235                           card >= min_sym_break_card andalso
   3.236 @@ -1784,13 +1784,13 @@
   3.237                                   o binder_types o snd o #const) constrs)
   3.238             |> filter_out
   3.239                    (fn {typ, ...} =>
   3.240 -                      exists (is_datatype_in_needed_value typ) need_us)
   3.241 +                      exists (is_data_type_in_needed_value typ) need_us)
   3.242             |> (fn dtypes' =>
   3.243                    dtypes' |> length dtypes' > datatype_sym_break
   3.244 -                             ? (sort (datatype_ord o swap)
   3.245 +                             ? (sort (data_type_ord o swap)
   3.246                                  #> take datatype_sym_break))
   3.247 -           |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table
   3.248 -                                                  nfas dtypes)
   3.249 +           |> maps (sym_break_axioms_for_data_type hol_ctxt binarize kk rel_table
   3.250 +                                                   nfas dtypes)
   3.251  
   3.252  fun sel_axioms_for_sel hol_ctxt binarize j0
   3.253          (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
   3.254 @@ -1849,8 +1849,8 @@
   3.255        end
   3.256    end
   3.257  
   3.258 -fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table need_vals
   3.259 -                            (dtype as {constrs, ...}) =
   3.260 +fun sel_axioms_for_data_type hol_ctxt binarize bits j0 kk rel_table need_vals
   3.261 +                             (dtype as {constrs, ...}) =
   3.262    maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table need_vals
   3.263                                dtype) constrs
   3.264  
   3.265 @@ -1879,14 +1879,14 @@
   3.266                     (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))]
   3.267    end
   3.268  
   3.269 -fun uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
   3.270 -                                   (dtype as {constrs, ...}) =
   3.271 +fun uniqueness_axioms_for_data_type hol_ctxt binarize kk need_vals rel_table
   3.272 +                                    (dtype as {constrs, ...}) =
   3.273    maps (uniqueness_axioms_for_constr hol_ctxt binarize kk need_vals rel_table
   3.274                                       dtype) constrs
   3.275  
   3.276  fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta
   3.277  
   3.278 -fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...})
   3.279 +fun partition_axioms_for_data_type j0 (kk as {kk_rel_eq, kk_union, ...})
   3.280          need_vals rel_table (dtype as {card, constrs, ...}) =
   3.281    if forall #exclusive constrs then
   3.282      [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool]
   3.283 @@ -1898,31 +1898,31 @@
   3.284         kk_disjoint_sets kk rs]
   3.285      end
   3.286  
   3.287 -fun other_axioms_for_datatype _ _ _ _ _ _ _ {deep = false, ...} = []
   3.288 -  | other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk rel_table
   3.289 -                              (dtype as {typ, ...}) =
   3.290 +fun other_axioms_for_data_type _ _ _ _ _ _ _ {deep = false, ...} = []
   3.291 +  | other_axioms_for_data_type hol_ctxt binarize need_vals bits ofs kk rel_table
   3.292 +                               (dtype as {typ, ...}) =
   3.293      let val j0 = offset_of_type ofs typ in
   3.294 -      sel_axioms_for_datatype hol_ctxt binarize bits j0 kk need_vals rel_table
   3.295 -                              dtype @
   3.296 -      uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table
   3.297 -                                     dtype @
   3.298 -      partition_axioms_for_datatype j0 kk need_vals rel_table dtype
   3.299 +      sel_axioms_for_data_type hol_ctxt binarize bits j0 kk need_vals rel_table
   3.300 +                               dtype @
   3.301 +      uniqueness_axioms_for_data_type hol_ctxt binarize kk need_vals rel_table
   3.302 +                                      dtype @
   3.303 +      partition_axioms_for_data_type j0 kk need_vals rel_table dtype
   3.304      end
   3.305  
   3.306 -fun declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
   3.307 +fun declarative_axioms_for_data_types hol_ctxt binarize need_us need_vals
   3.308          datatype_sym_break bits ofs kk rel_table dtypes =
   3.309    let
   3.310      val nfas =
   3.311 -      dtypes |> map_filter (nfa_entry_for_datatype hol_ctxt binarize kk
   3.312 -                                                   rel_table dtypes)
   3.313 +      dtypes |> map_filter (nfa_entry_for_data_type hol_ctxt binarize kk
   3.314 +                                                    rel_table dtypes)
   3.315               |> strongly_connected_sub_nfas
   3.316    in
   3.317 -    acyclicity_axioms_for_datatypes kk nfas @
   3.318 -    maps (needed_value_axioms_for_datatype ofs kk dtypes) need_vals @
   3.319 -    sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
   3.320 -                                   kk rel_table nfas dtypes @
   3.321 -    maps (other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk
   3.322 -                                    rel_table) dtypes
   3.323 +    acyclicity_axioms_for_data_types kk nfas @
   3.324 +    maps (needed_value_axioms_for_data_type ofs kk dtypes) need_vals @
   3.325 +    sym_break_axioms_for_data_types hol_ctxt binarize need_us datatype_sym_break
   3.326 +                                    kk rel_table nfas dtypes @
   3.327 +    maps (other_axioms_for_data_type hol_ctxt binarize need_vals bits ofs kk
   3.328 +                                     rel_table) dtypes
   3.329    end
   3.330  
   3.331  end;
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 03 22:33:22 2014 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 03 22:33:22 2014 +0100
     4.3 @@ -367,7 +367,7 @@
     4.4  and reconstruct_term maybe_opt unfold pool
     4.5          (wacky_names as ((maybe_name, abs_name), _))
     4.6          (scope as {hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits,
     4.7 -                   datatypes, ofs, ...})
     4.8 +                   data_types, ofs, ...})
     4.9          atomss sel_names rel_table bounds =
    4.10    let
    4.11      val for_auto = (maybe_name = "")
    4.12 @@ -403,7 +403,7 @@
    4.13          val empty_const = Const (@{const_abbrev Set.empty}, set_T)
    4.14          val insert_const = Const (@{const_name insert}, T --> set_T --> set_T)
    4.15          fun aux [] =
    4.16 -            if maybe_opt andalso not (is_complete_type datatypes false T) then
    4.17 +            if maybe_opt andalso not (is_complete_type data_types false T) then
    4.18                insert_const $ Const (unrep (), T) $ empty_const
    4.19              else
    4.20                empty_const
    4.21 @@ -432,7 +432,7 @@
    4.22                 Const (@{const_name None}, _) => aux' tps
    4.23               | _ => update_const $ aux' tps $ t1 $ t2)
    4.24          fun aux tps =
    4.25 -          if maybe_opt andalso not (is_complete_type datatypes false T1) then
    4.26 +          if maybe_opt andalso not (is_complete_type data_types false T1) then
    4.27              update_const $ aux' tps $ Const (unrep (), T1)
    4.28              $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
    4.29            else
    4.30 @@ -463,7 +463,7 @@
    4.31               | Const (s, Type (@{type_name fun}, [T1, T2])) =>
    4.32                 if s = opt_flag orelse s = non_opt_flag then
    4.33                   Abs ("x", T1,
    4.34 -                      Const (if is_complete_type datatypes false T1 then
    4.35 +                      Const (if is_complete_type data_types false T1 then
    4.36                                 irrelevant
    4.37                               else
    4.38                                 unknown, T2))
    4.39 @@ -525,7 +525,7 @@
    4.40            HOLogic.mk_number nat_T (k - j - 1)
    4.41          else if T = @{typ bisim_iterator} then
    4.42            HOLogic.mk_number nat_T j
    4.43 -        else case datatype_spec datatypes T of
    4.44 +        else case data_type_spec data_types T of
    4.45            NONE => nth_atom thy atomss pool for_auto T j
    4.46          | SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j
    4.47          | SOME {co, constrs, ...} =>
    4.48 @@ -888,7 +888,7 @@
    4.49                        simp_table, psimp_table, choice_spec_table, intro_table,
    4.50                        ground_thm_table, ersatz_table, skolems, special_funs,
    4.51                        unrolled_preds, wf_cache, constr_cache}, binarize,
    4.52 -                      card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
    4.53 +                      card_assigns, bits, bisim_depth, data_types, ofs} : scope)
    4.54          formats atomss real_frees pseudo_frees free_names sel_names nonsel_names
    4.55          rel_table bounds =
    4.56    let
    4.57 @@ -910,15 +910,16 @@
    4.58         wf_cache = wf_cache, constr_cache = constr_cache}
    4.59      val scope =
    4.60        {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    4.61 -       bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
    4.62 +       bits = bits, bisim_depth = bisim_depth, data_types = data_types,
    4.63 +       ofs = ofs}
    4.64      fun term_for_rep maybe_opt unfold =
    4.65        reconstruct_term maybe_opt unfold pool wacky_names scope atomss
    4.66                         sel_names rel_table bounds
    4.67      val all_values =
    4.68        all_values_of_type pool wacky_names scope atomss sel_names rel_table
    4.69                           bounds
    4.70 -    fun is_codatatype_wellformed (cos : datatype_spec list)
    4.71 -                                 ({typ, card, ...} : datatype_spec) =
    4.72 +    fun is_codatatype_wellformed (cos : data_type_spec list)
    4.73 +                                 ({typ, card, ...} : data_type_spec) =
    4.74        let
    4.75          val ts = all_values card typ
    4.76          val max_depth = Integer.sum (map #card cos)
    4.77 @@ -950,7 +951,7 @@
    4.78              [Syntax.pretty_term ctxt t1, Pretty.str oper,
    4.79               Syntax.pretty_term ctxt t2])
    4.80        end
    4.81 -    fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
    4.82 +    fun pretty_for_data_type ({typ, card, complete, ...} : data_type_spec) =
    4.83        Pretty.block (Pretty.breaks
    4.84            (pretty_for_type ctxt typ ::
    4.85             (case typ of
    4.86 @@ -962,24 +963,18 @@
    4.87                  (map (Syntax.pretty_term ctxt) (all_values card typ) @
    4.88                   (if fun_from_pair complete false then []
    4.89                    else [Pretty.str (unrep ())]))]))
    4.90 -    fun integer_datatype T =
    4.91 +    fun integer_data_type T =
    4.92        [{typ = T, card = card_of_type card_assigns T, co = false,
    4.93          self_rec = true, complete = (false, false), concrete = (true, true),
    4.94          deep = true, constrs = []}]
    4.95        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    4.96 -    val (codatatypes, datatypes) =
    4.97 -      datatypes |> filter #deep |> List.partition #co
    4.98 -                ||> append (integer_datatype nat_T @ integer_datatype int_T)
    4.99 -    val block_of_datatypes =
   4.100 -      if show_types andalso not (null datatypes) then
   4.101 -        [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
   4.102 -                         (map pretty_for_datatype datatypes)]
   4.103 -      else
   4.104 -        []
   4.105 -    val block_of_codatatypes =
   4.106 -      if show_types andalso not (null codatatypes) then
   4.107 -        [Pretty.big_list ("Codatatype" ^ plural_s_for_list codatatypes ^ ":")
   4.108 -                         (map pretty_for_datatype codatatypes)]
   4.109 +    val data_types =
   4.110 +      data_types |> filter #deep
   4.111 +                 |> append (maps integer_data_type [nat_T, int_T])
   4.112 +    val block_of_data_types =
   4.113 +      if show_types andalso not (null data_types) then
   4.114 +        [Pretty.big_list ("Type" ^ plural_s_for_list data_types ^ ":")
   4.115 +                         (map pretty_for_data_type data_types)]
   4.116        else
   4.117          []
   4.118      fun block_of_names show title names =
   4.119 @@ -1010,9 +1005,10 @@
   4.120      val chunks = block_of_names true "Free variable" real_free_names @
   4.121                   block_of_names show_skolems "Skolem constant" skolem_names @
   4.122                   block_of_names true "Evaluated term" eval_names @
   4.123 -                 block_of_datatypes @ block_of_codatatypes @
   4.124 +                 block_of_data_types @
   4.125                   block_of_names show_consts "Constant"
   4.126                                  noneval_nonskolem_nonsel_names
   4.127 +    val codatatypes = filter #co data_types;
   4.128    in
   4.129      (Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"]
   4.130                      else chunks),
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Mar 03 22:33:22 2014 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Mar 03 22:33:22 2014 +0100
     5.3 @@ -41,7 +41,7 @@
     5.4     binarize: bool,
     5.5     alpha_T: typ,
     5.6     max_fresh: int Unsynchronized.ref,
     5.7 -   datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
     5.8 +   data_type_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
     5.9     constr_mcache: ((string * typ) * mtyp) list Unsynchronized.ref}
    5.10  
    5.11  exception UNSOLVABLE of unit
    5.12 @@ -123,7 +123,7 @@
    5.13  
    5.14  fun initial_mdata hol_ctxt binarize alpha_T =
    5.15    ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
    5.16 -    max_fresh = Unsynchronized.ref 0, datatype_mcache = Unsynchronized.ref [],
    5.17 +    max_fresh = Unsynchronized.ref 0, data_type_mcache = Unsynchronized.ref [],
    5.18      constr_mcache = Unsynchronized.ref []} : mdata)
    5.19  
    5.20  fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
    5.21 @@ -134,7 +134,7 @@
    5.22  fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
    5.23      could_exist_alpha_subtype alpha_T T
    5.24    | could_exist_alpha_sub_mtype ctxt alpha_T T =
    5.25 -    (T = alpha_T orelse is_datatype ctxt T)
    5.26 +    (T = alpha_T orelse is_data_type ctxt T)
    5.27  
    5.28  fun exists_alpha_sub_mtype MAlpha = true
    5.29    | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
    5.30 @@ -170,7 +170,7 @@
    5.31      | M => if member (op =) seen M then MType (s, [])
    5.32             else repair_mtype cache (M :: seen) M
    5.33  
    5.34 -fun repair_datatype_mcache cache =
    5.35 +fun repair_data_type_mcache cache =
    5.36    let
    5.37      fun repair_one (z, M) =
    5.38        Unsynchronized.change cache
    5.39 @@ -219,7 +219,7 @@
    5.40                 A Gen
    5.41    in (M1, aa, M2) end
    5.42  and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
    5.43 -                                    datatype_mcache, constr_mcache, ...})
    5.44 +                                    data_type_mcache, constr_mcache, ...})
    5.45                           all_minus =
    5.46    let
    5.47      fun do_type T =
    5.48 @@ -232,12 +232,12 @@
    5.49        | Type (@{type_name set}, [T']) => do_type (T' --> bool_T)
    5.50        | Type (z as (s, _)) =>
    5.51          if could_exist_alpha_sub_mtype ctxt alpha_T T then
    5.52 -          case AList.lookup (op =) (!datatype_mcache) z of
    5.53 +          case AList.lookup (op =) (!data_type_mcache) z of
    5.54              SOME M => M
    5.55            | NONE =>
    5.56              let
    5.57 -              val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
    5.58 -              val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
    5.59 +              val _ = Unsynchronized.change data_type_mcache (cons (z, MRec z))
    5.60 +              val xs = binarized_and_boxed_data_type_constrs hol_ctxt binarize T
    5.61                val (all_Ms, constr_Ms) =
    5.62                  fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
    5.63                               let
    5.64 @@ -252,15 +252,15 @@
    5.65                               end)
    5.66                           xs ([], [])
    5.67                val M = MType (s, all_Ms)
    5.68 -              val _ = Unsynchronized.change datatype_mcache
    5.69 +              val _ = Unsynchronized.change data_type_mcache
    5.70                            (AList.update (op =) (z, M))
    5.71                val _ = Unsynchronized.change constr_mcache
    5.72                            (append (xs ~~ constr_Ms))
    5.73              in
    5.74 -              if forall (not o is_MRec o snd) (!datatype_mcache) then
    5.75 -                (repair_datatype_mcache datatype_mcache;
    5.76 -                 repair_constr_mcache (!datatype_mcache) constr_mcache;
    5.77 -                 AList.lookup (op =) (!datatype_mcache) z |> the)
    5.78 +              if forall (not o is_MRec o snd) (!data_type_mcache) then
    5.79 +                (repair_data_type_mcache data_type_mcache;
    5.80 +                 repair_constr_mcache (!data_type_mcache) constr_mcache;
    5.81 +                 AList.lookup (op =) (!data_type_mcache) z |> the)
    5.82                else
    5.83                  M
    5.84              end
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 03 22:33:22 2014 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 03 22:33:22 2014 +0100
     6.3 @@ -702,12 +702,12 @@
     6.4    fold_rev (choose_rep_for_nth_sel_for_constr scope x)
     6.5             (~1 upto num_sels_for_constr_type T - 1)
     6.6  
     6.7 -fun choose_rep_for_sels_of_datatype _ ({deep = false, ...} : datatype_spec) = I
     6.8 -  | choose_rep_for_sels_of_datatype scope {constrs, ...} =
     6.9 +fun choose_rep_for_sels_of_data_type _ ({deep = false, ...} : data_type_spec) = I
    6.10 +  | choose_rep_for_sels_of_data_type scope {constrs, ...} =
    6.11      fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs
    6.12  
    6.13 -fun choose_reps_for_all_sels (scope as {datatypes, ...}) =
    6.14 -  fold (choose_rep_for_sels_of_datatype scope) datatypes o pair []
    6.15 +fun choose_reps_for_all_sels (scope as {data_types, ...}) =
    6.16 +  fold (choose_rep_for_sels_of_data_type scope) data_types o pair []
    6.17  
    6.18  val min_univ_card = 2
    6.19  
    6.20 @@ -813,7 +813,7 @@
    6.21  fun untuple f (Tuple (_, _, us)) = maps (untuple f) us
    6.22    | untuple f u = [f u]
    6.23  
    6.24 -fun choose_reps_in_nut (scope as {card_assigns, bits, datatypes, ofs, ...})
    6.25 +fun choose_reps_in_nut (scope as {card_assigns, bits, data_types, ofs, ...})
    6.26                         unsound table def =
    6.27    let
    6.28      val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
    6.29 @@ -924,7 +924,7 @@
    6.30              if is_opt_rep R then
    6.31                triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
    6.32              else if not opt orelse unsound orelse polar = Neg orelse
    6.33 -                    is_concrete_type datatypes true (type_of u1) then
    6.34 +                    is_concrete_type data_types true (type_of u1) then
    6.35                s_op2 Subset T R u1 u2
    6.36              else
    6.37                Cst (False, T, Formula Pos)
    6.38 @@ -947,7 +947,7 @@
    6.39                else opt_opt_case ()
    6.40            in
    6.41              if unsound orelse polar = Neg orelse
    6.42 -               is_concrete_type datatypes true (type_of u1) then
    6.43 +               is_concrete_type data_types true (type_of u1) then
    6.44                case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
    6.45                  (true, true) => opt_opt_case ()
    6.46                | (true, false) => hybrid_case u1'
    6.47 @@ -1002,7 +1002,7 @@
    6.48                  let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
    6.49                    if def orelse
    6.50                       (unsound andalso (polar = Pos) = (oper = All)) orelse
    6.51 -                     is_complete_type datatypes true (type_of u1) then
    6.52 +                     is_complete_type data_types true (type_of u1) then
    6.53                      quant_u
    6.54                    else
    6.55                      let
    6.56 @@ -1072,7 +1072,7 @@
    6.57              val Rs = map rep_of us
    6.58              val R = best_one_rep_for_type scope T
    6.59              val {total, ...} =
    6.60 -              constr_spec datatypes (original_name (nickname_of (hd us')), T)
    6.61 +              constr_spec data_types (original_name (nickname_of (hd us')), T)
    6.62              val opt = exists is_opt_rep Rs orelse not total
    6.63            in Construct (map sub us', T, R |> opt ? Opt, us) end
    6.64          | _ =>
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Mar 03 22:33:22 2014 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Mar 03 22:33:22 2014 +0100
     7.3 @@ -274,8 +274,8 @@
     7.4      best_non_opt_set_rep_for_type scope (T' --> bool_T)
     7.5    | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
     7.6  
     7.7 -fun best_set_rep_for_type (scope as {datatypes, ...}) T =
     7.8 -  (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
     7.9 +fun best_set_rep_for_type (scope as {data_types, ...}) T =
    7.10 +  (if is_exact_type data_types true T then best_non_opt_set_rep_for_type
    7.11     else best_opt_set_rep_for_type) scope T
    7.12  
    7.13  fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Mar 03 22:33:22 2014 +0100
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Mar 03 22:33:22 2014 +0100
     8.3 @@ -17,7 +17,7 @@
     8.4       explicit_max: int,
     8.5       total: bool}
     8.6  
     8.7 -  type datatype_spec =
     8.8 +  type data_type_spec =
     8.9      {typ: typ,
    8.10       card: int,
    8.11       co: bool,
    8.12 @@ -33,15 +33,15 @@
    8.13       card_assigns: (typ * int) list,
    8.14       bits: int,
    8.15       bisim_depth: int,
    8.16 -     datatypes: datatype_spec list,
    8.17 +     data_types: data_type_spec list,
    8.18       ofs: int Typtab.table}
    8.19  
    8.20 -  val is_asymmetric_nondatatype : typ -> bool
    8.21 -  val datatype_spec : datatype_spec list -> typ -> datatype_spec option
    8.22 -  val constr_spec : datatype_spec list -> string * typ -> constr_spec
    8.23 -  val is_complete_type : datatype_spec list -> bool -> typ -> bool
    8.24 -  val is_concrete_type : datatype_spec list -> bool -> typ -> bool
    8.25 -  val is_exact_type : datatype_spec list -> bool -> typ -> bool
    8.26 +  val is_asymmetric_non_data_type : typ -> bool
    8.27 +  val data_type_spec : data_type_spec list -> typ -> data_type_spec option
    8.28 +  val constr_spec : data_type_spec list -> string * typ -> constr_spec
    8.29 +  val is_complete_type : data_type_spec list -> bool -> typ -> bool
    8.30 +  val is_concrete_type : data_type_spec list -> bool -> typ -> bool
    8.31 +  val is_exact_type : data_type_spec list -> bool -> typ -> bool
    8.32    val offset_of_type : int Typtab.table -> typ -> int
    8.33    val spec_of_type : scope -> typ -> int * int
    8.34    val pretties_for_scope : scope -> bool -> Pretty.T list
    8.35 @@ -70,7 +70,7 @@
    8.36     explicit_max: int,
    8.37     total: bool}
    8.38  
    8.39 -type datatype_spec =
    8.40 +type data_type_spec =
    8.41    {typ: typ,
    8.42     card: int,
    8.43     co: bool,
    8.44 @@ -86,7 +86,7 @@
    8.45     card_assigns: (typ * int) list,
    8.46     bits: int,
    8.47     bisim_depth: int,
    8.48 -   datatypes: datatype_spec list,
    8.49 +   data_types: data_type_spec list,
    8.50     ofs: int Typtab.table}
    8.51  
    8.52  datatype row_kind = Card of typ | Max of string * typ
    8.53 @@ -94,14 +94,14 @@
    8.54  type row = row_kind * int list
    8.55  type block = row list
    8.56  
    8.57 -val is_asymmetric_nondatatype =
    8.58 +val is_asymmetric_non_data_type =
    8.59    is_iterator_type orf is_integer_type orf is_bit_type
    8.60  
    8.61 -fun datatype_spec (dtypes : datatype_spec list) T =
    8.62 +fun data_type_spec (dtypes : data_type_spec list) T =
    8.63    List.find (curry (op =) T o #typ) dtypes
    8.64  
    8.65  fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
    8.66 -  | constr_spec ({constrs, ...} :: dtypes : datatype_spec list) (x as (s, T)) =
    8.67 +  | constr_spec ({constrs, ...} :: dtypes : data_type_spec list) (x as (s, T)) =
    8.68      case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const))
    8.69                     constrs of
    8.70        SOME c => c
    8.71 @@ -115,7 +115,7 @@
    8.72      is_concrete_type dtypes facto T'
    8.73    | is_complete_type dtypes facto T =
    8.74      not (is_integer_like_type T) andalso not (is_bit_type T) andalso
    8.75 -    fun_from_pair (#complete (the (datatype_spec dtypes T))) facto
    8.76 +    fun_from_pair (#complete (the (data_type_spec dtypes T))) facto
    8.77      handle Option.Option => true
    8.78  and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
    8.79      is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
    8.80 @@ -124,7 +124,7 @@
    8.81    | is_concrete_type dtypes facto (Type (@{type_name set}, [T'])) =
    8.82      is_complete_type dtypes facto T'
    8.83    | is_concrete_type dtypes facto T =
    8.84 -    fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
    8.85 +    fun_from_pair (#concrete (the (data_type_spec dtypes T))) facto
    8.86      handle Option.Option => true
    8.87  and is_exact_type dtypes facto =
    8.88    is_complete_type dtypes facto andf is_concrete_type dtypes facto
    8.89 @@ -140,7 +140,7 @@
    8.90  
    8.91  fun quintuple_for_scope code_type code_term code_string
    8.92          ({hol_ctxt = {ctxt, ...}, card_assigns, bits, bisim_depth,
    8.93 -         datatypes, ...} : scope) =
    8.94 +         data_types, ...} : scope) =
    8.95    let
    8.96      val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
    8.97                       @{typ bisim_iterator}]
    8.98 @@ -149,7 +149,7 @@
    8.99                     |> List.partition (is_fp_iterator_type o fst)
   8.100      val (secondary_card_assigns, primary_card_assigns) =
   8.101        card_assigns
   8.102 -      |> List.partition ((is_integer_type orf is_datatype ctxt) o fst)
   8.103 +      |> List.partition ((is_integer_type orf is_data_type ctxt) o fst)
   8.104      val cards =
   8.105        map (fn (T, k) =>
   8.106                [code_type ctxt T, code_string (" = " ^ string_of_int k)])
   8.107 @@ -161,7 +161,7 @@
   8.108                      else
   8.109                        SOME [code_term ctxt (Const const),
   8.110                              code_string (" = " ^ string_of_int explicit_max)])
   8.111 -                 o #constrs) datatypes
   8.112 +                 o #constrs) data_types
   8.113      fun iters () =
   8.114        map (fn (T, k) =>
   8.115                [code_term ctxt (Const (const_for_iterator_type T)),
   8.116 @@ -169,7 +169,7 @@
   8.117      fun miscs () =
   8.118        (if bits = 0 then []
   8.119         else [code_string ("bits = " ^ string_of_int bits)]) @
   8.120 -      (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
   8.121 +      (if bisim_depth < 0 andalso forall (not o #co) data_types then []
   8.122         else [code_string ("bisim_depth = " ^ signed_string_of_int bisim_depth)])
   8.123    in
   8.124      (cards primary_card_assigns, cards secondary_card_assigns,
   8.125 @@ -210,7 +210,7 @@
   8.126    end
   8.127  
   8.128  fun scopes_equivalent (s1 : scope, s2 : scope) =
   8.129 -  #datatypes s1 = #datatypes s2 andalso #card_assigns s1 = #card_assigns s2
   8.130 +  #data_types s1 = #data_types s2 andalso #card_assigns s1 = #card_assigns s2
   8.131  
   8.132  fun scope_less_eq (s1 : scope) (s2 : scope) =
   8.133    (s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=)
   8.134 @@ -265,7 +265,7 @@
   8.135                                                (const_for_iterator_type T)))]
   8.136      else
   8.137        (Card T, lookup_type_ints_assign thy cards_assigns T) ::
   8.138 -      (case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
   8.139 +      (case binarized_and_boxed_data_type_constrs hol_ctxt binarize T of
   8.140           [_] => []
   8.141         | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
   8.142  
   8.143 @@ -304,7 +304,7 @@
   8.144  
   8.145  fun is_surely_inconsistent_card_assign hol_ctxt binarize
   8.146                                         (card_assigns, max_assigns) (T, k) =
   8.147 -  case binarized_and_boxed_datatype_constrs hol_ctxt binarize T of
   8.148 +  case binarized_and_boxed_data_type_constrs hol_ctxt binarize T of
   8.149      [] => false
   8.150    | xs =>
   8.151      let
   8.152 @@ -376,9 +376,9 @@
   8.153    let
   8.154      fun aux next _ [] = Typtab.update_new (dummyT, next)
   8.155        | aux next reusable ((T, k) :: assigns) =
   8.156 -        if k = 1 orelse is_asymmetric_nondatatype T then
   8.157 +        if k = 1 orelse is_asymmetric_non_data_type T then
   8.158            aux next reusable assigns
   8.159 -        else if length (these (Option.map #constrs (datatype_spec dtypes T)))
   8.160 +        else if length (these (Option.map #constrs (data_type_spec dtypes T)))
   8.161                  > 1 then
   8.162            Typtab.update_new (T, next) #> aux (next + k) reusable assigns
   8.163          else
   8.164 @@ -439,13 +439,13 @@
   8.165                 card_assigns T
   8.166    end
   8.167  
   8.168 -fun datatype_spec_from_scope_descriptor (hol_ctxt as {ctxt, ...})
   8.169 +fun data_type_spec_from_scope_descriptor (hol_ctxt as {ctxt, ...})
   8.170          binarize deep_dataTs finitizable_dataTs (desc as (card_assigns, _))
   8.171          (T, card) =
   8.172    let
   8.173      val deep = member (op =) deep_dataTs T
   8.174      val co = is_codatatype ctxt T
   8.175 -    val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
   8.176 +    val xs = binarized_and_boxed_data_type_constrs hol_ctxt binarize T
   8.177      val self_recs = map (is_self_recursive_constr_type o snd) xs
   8.178      val (num_self_recs, num_non_self_recs) =
   8.179        List.partition I self_recs |> pairself length
   8.180 @@ -475,10 +475,10 @@
   8.181  fun scope_from_descriptor (hol_ctxt as {ctxt, ...}) binarize deep_dataTs
   8.182                            finitizable_dataTs (desc as (card_assigns, _)) =
   8.183    let
   8.184 -    val datatypes =
   8.185 -      map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
   8.186 -                                               finitizable_dataTs desc)
   8.187 -          (filter (is_datatype ctxt o fst) card_assigns)
   8.188 +    val data_types =
   8.189 +      map (data_type_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
   8.190 +                                                finitizable_dataTs desc)
   8.191 +          (filter (is_data_type ctxt o fst) card_assigns)
   8.192      val bits = card_of_type card_assigns @{typ signed_bit} - 1
   8.193                 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
   8.194                        card_of_type card_assigns @{typ unsigned_bit}
   8.195 @@ -486,8 +486,8 @@
   8.196      val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
   8.197    in
   8.198      {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
   8.199 -     datatypes = datatypes, bits = bits, bisim_depth = bisim_depth,
   8.200 -     ofs = offset_table_for_card_assigns datatypes card_assigns}
   8.201 +     data_types = data_types, bits = bits, bisim_depth = bisim_depth,
   8.202 +     ofs = offset_table_for_card_assigns data_types card_assigns}
   8.203    end
   8.204  
   8.205  fun repair_cards_assigns_wrt_boxing_etc _ _ [] = []