src/HOL/Tools/record_package.ML

 
 (** record simproc **)
 
 local
 
-val sel_upd_pat = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s (u k r)", HOLogic.termT)];
+val sel_upd_pat = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s (u k r)"];
 
 fun proc sg _ t =
   (case t of (sel as Const (s, _)) $ ((upd as Const (u, _)) $ k $ r) =>
     (case get_selectors sg s of Some () =>
       (case get_updates sg u of Some u_name =>

 (* field_typedefs *)
 
 fun field_typedefs zeta moreT names theory =
   let
     val alpha = "'a";
-    val aT = TFree (alpha, HOLogic.termS);
+    val aT = TFree (alpha, HOLogic.typeS);
     val UNIV = HOLogic.mk_UNIV (HOLogic.mk_prodT (aT, moreT));
 
     fun type_def (thy, name) =
       let val (thy', {type_definition, set_def = Some def, ...}) =
         thy |> setmp TypedefPackage.quiet_mode true

   let
     val sign = Theory.sign_of thy;
     val base = Sign.base_name;
     val full_path = Sign.full_name_path sign;
 
-    val xT = TFree (variant alphas "'x", HOLogic.termS);
+    val xT = TFree (variant alphas "'x", HOLogic.typeS);
 
 
     (* prepare declarations and definitions *)
 
     (*field constructors*)

     val all_xs = parent_xs @ xs;
     val all_vars = parent_vars @ vars;
     val all_named_vars = parent_named_vars @ named_vars;
 
     val zeta = variant alphas "'z";
-    val moreT = TFree (zeta, HOLogic.termS);
+    val moreT = TFree (zeta, HOLogic.typeS);
     val more = Free (moreN, moreT);
     val full_moreN = full moreN;
     fun more_part t = mk_more t full_moreN;
     fun more_part_update t x = mk_more_update t (full_moreN, x);
     val all_types_more = all_types @ [moreT];