src/HOL/Tools/record.ML

 
 fun read_typ ctxt raw_T env =
   let
     val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
     val T = Syntax.read_typ ctxt' raw_T;
-    val env' = OldTerm.add_typ_tfrees (T, env);
+    val env' = Misc_Legacy.add_typ_tfrees (T, env);
   in (T, env') end;
 
 fun cert_typ ctxt raw_T env =
   let
     val thy = Proof_Context.theory_of ctxt;
     val T = Type.no_tvars (Sign.certify_typ thy raw_T)
       handle TYPE (msg, _, _) => error msg;
-    val env' = OldTerm.add_typ_tfrees (T, env);
+    val env' = Misc_Legacy.add_typ_tfrees (T, env);
   in (T, env') end;
 
 
 (* attributes *)