src/HOL/Tools/datatype_prop.ML

     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val used = foldr add_typ_tfree_names (recTs, []);
 
     val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
-      replicate (length descr') HOLogic.termS);
+      replicate (length descr') HOLogic.typeS);
 
     val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let
           val Ts = map (typ_of_dtyp descr' sorts) cargs;

   let
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val used = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
-    val T' = TFree (variant used "'t", HOLogic.termS);
+    val T' = TFree (variant used "'t", HOLogic.typeS);
 
     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
       map (fn (_, cargs) =>
         let val Ts = map (typ_of_dtyp descr' sorts) cargs
         in Ts ---> T' end) constrs) (hd descr);

   let
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
     val used' = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
-    val T' = TFree (variant used' "'t", HOLogic.termS);
+    val T' = TFree (variant used' "'t", HOLogic.typeS);
     val P = Free ("P", T' --> HOLogic.boolT);
 
     fun make_split (((_, (_, _, constrs)), T), comb_t) =
       let
         val (_, fs) = strip_comb comb_t;