src/HOL/Tools/Nitpick/nitpick_mono.ML

 type mdata =
   {hol_ctxt: hol_context,
    binarize: bool,
    alpha_T: typ,
    max_fresh: int Unsynchronized.ref,
-   datatype_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
+   data_type_mcache: ((string * typ list) * mtyp) list Unsynchronized.ref,
    constr_mcache: ((string * typ) * mtyp) list Unsynchronized.ref}
 
 exception UNSOLVABLE of unit
 exception MTYPE of string * mtyp list * typ list
 

   | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
   | flatten_mtype M = [M]
 
 fun initial_mdata hol_ctxt binarize alpha_T =
   ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
-    max_fresh = Unsynchronized.ref 0, datatype_mcache = Unsynchronized.ref [],
+    max_fresh = Unsynchronized.ref 0, data_type_mcache = Unsynchronized.ref [],
     constr_mcache = Unsynchronized.ref []} : mdata)
 
 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
     T = alpha_T orelse (not (is_fp_iterator_type T) andalso
                         exists (could_exist_alpha_subtype alpha_T) Ts)
   | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
 
 fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
     could_exist_alpha_subtype alpha_T T
   | could_exist_alpha_sub_mtype ctxt alpha_T T =
-    (T = alpha_T orelse is_datatype ctxt T)
+    (T = alpha_T orelse is_data_type ctxt T)
 
 fun exists_alpha_sub_mtype MAlpha = true
   | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
     exists exists_alpha_sub_mtype [M1, M2]
   | exists_alpha_sub_mtype (MPair (M1, M2)) =

     case AList.lookup (op =) cache z |> the of
       MRec _ => MType (s, [])
     | M => if member (op =) seen M then MType (s, [])
            else repair_mtype cache (M :: seen) M
 
-fun repair_datatype_mcache cache =
+fun repair_data_type_mcache cache =
   let
     fun repair_one (z, M) =
       Unsynchronized.change cache
           (AList.update (op =) (z, repair_mtype (!cache) [] M))
   in List.app repair_one (rev (!cache)) end

                V (Unsynchronized.inc max_fresh)
              else
                A Gen
   in (M1, aa, M2) end
 and fresh_mtype_for_type (mdata as {hol_ctxt as {ctxt, ...}, binarize, alpha_T,
-                                    datatype_mcache, constr_mcache, ...})
+                                    data_type_mcache, constr_mcache, ...})
                          all_minus =
   let
     fun do_type T =
       if T = alpha_T then
         MAlpha

         MFun (fresh_mfun_for_fun_type mdata all_minus T1 T2)
       | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
       | Type (@{type_name set}, [T']) => do_type (T' --> bool_T)
       | Type (z as (s, _)) =>
         if could_exist_alpha_sub_mtype ctxt alpha_T T then
-          case AList.lookup (op =) (!datatype_mcache) z of
+          case AList.lookup (op =) (!data_type_mcache) z of
             SOME M => M
           | NONE =>
             let
-              val _ = Unsynchronized.change datatype_mcache (cons (z, MRec z))
-              val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
+              val _ = Unsynchronized.change data_type_mcache (cons (z, MRec z))
+              val xs = binarized_and_boxed_data_type_constrs hol_ctxt binarize T
               val (all_Ms, constr_Ms) =
                 fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
                              let
                                val binder_Ms = map do_type (binder_types T')
                                val new_Ms = filter exists_alpha_sub_mtype_fresh

                                (union (op =) new_Ms all_Ms,
                                 constr_M :: constr_Ms)
                              end)
                          xs ([], [])
               val M = MType (s, all_Ms)
-              val _ = Unsynchronized.change datatype_mcache
+              val _ = Unsynchronized.change data_type_mcache
                           (AList.update (op =) (z, M))
               val _ = Unsynchronized.change constr_mcache
                           (append (xs ~~ constr_Ms))
             in
-              if forall (not o is_MRec o snd) (!datatype_mcache) then
-                (repair_datatype_mcache datatype_mcache;
-                 repair_constr_mcache (!datatype_mcache) constr_mcache;
-                 AList.lookup (op =) (!datatype_mcache) z |> the)
+              if forall (not o is_MRec o snd) (!data_type_mcache) then
+                (repair_data_type_mcache data_type_mcache;
+                 repair_constr_mcache (!data_type_mcache) constr_mcache;
+                 AList.lookup (op =) (!data_type_mcache) z |> the)
               else
                 M
             end
         else
           MType (s, [])