src/HOL/Tools/datatype_package.ML

                 else None
           | _ => None)
    | _ => None)
   | distinct_proc sg _ _ = None;
 
-val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termT)];
+val distinct_pats = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s = t"];
 val distinct_simproc = mk_simproc distinctN distinct_pats distinct_proc;
 
 val dist_ss = HOL_ss addsimprocs [distinct_simproc];
 
 val simproc_setup =

       map (fn ((_, cargs), (cname, mx)) =>
         (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
           (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
 
     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;

         (1 upto (length descr')));
 
     val size_names = DatatypeProp.indexify_names
       (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs)));
 
-    val freeT = TFree (variant used "'t", HOLogic.termS);
+    val freeT = 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 ---> freeT end) constrs) (hd descr);