src/HOL/Tools/Nitpick/nitpick_mono.ML

       if T = alpha_T then
         MAlpha
       else case T of
         Type (@{type_name fun}, [T1, T2]) =>
         MFun (fresh_mfun_for_fun_type mdata false T1 T2)
-      | Type (@{type_name Product_Type.prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
+      | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
       | Type (z as (s, _)) =>
         if could_exist_alpha_sub_mtype ctxt alpha_T T then
           case AList.lookup (op =) (!datatype_mcache) z of
             SOME M => M
           | NONE =>

           case (M, T) of
             (MAlpha, _) => T
           | (MFun (M1, a, M2), Type (@{type_name fun}, Ts)) =>
             Type (if should_finitize T a then @{type_name fin_fun}
                   else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
-          | (MPair (M1, M2), Type (@{type_name Product_Type.prod}, Ts)) =>
-            Type (@{type_name Product_Type.prod}, map2 type_from_mtype Ts [M1, M2])
+          | (MPair (M1, M2), Type (@{type_name prod}, Ts)) =>
+            Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2])
           | (MType _, _) => T
           | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
                               [M], [T])
         fun finitize_constr (x as (s, T)) =
           (s, case AList.lookup (op =) constr_mtypes x of