src/HOL/Tools/record.ML

                     val varifyT = varifyT midx;
                     val vartypes = map varifyT types;
 
                     val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
                       handle Type.TYPE_MATCH => err "type is no proper record (extension)";
-                    val term_of_typ = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
                     val alphas' =
-                      map (term_of_typ o Envir.norm_type subst o varifyT) (#1 (split_last alphas));
+                      map (Syntax_Phases.term_of_typ ctxt o Envir.norm_type subst o varifyT)
+                        (#1 (split_last alphas));
 
                     val more' = mk_ext rest;
                   in
                     list_comb
                       (Syntax.const (Syntax.mark_type (suffix ext_typeN ext)), alphas' @ [more'])

   let
     val thy = ProofContext.theory_of ctxt;
 
     val T = decode_type thy t;
     val varifyT = varifyT (Term.maxidx_of_typ T);
-
-    val term_of_type = Syntax_Phases.term_of_typ (Config.get ctxt show_sorts);
 
     fun strip_fields T =
       (case T of
         Type (ext, args as _ :: _) =>
           (case try (unsuffix ext_typeN) ext of

           | _ => [("", T)])
       | _ => [("", T)]);
 
     val (fields, (_, moreT)) = split_last (strip_fields T);
     val _ = null fields andalso raise Match;
-    val u = foldr1 field_types_tr' (map (field_type_tr' o apsnd term_of_type) fields);
+    val u =
+      foldr1 field_types_tr'
+        (map (field_type_tr' o apsnd (Syntax_Phases.term_of_typ ctxt)) fields);
   in
     if not (! print_type_as_fields) orelse null fields then raise Match
     else if moreT = HOLogic.unitT then Syntax.const @{syntax_const "_record_type"} $ u
-    else Syntax.const @{syntax_const "_record_type_scheme"} $ u $ term_of_type moreT
+    else
+      Syntax.const @{syntax_const "_record_type_scheme"} $ u $
+        Syntax_Phases.term_of_typ ctxt moreT
   end;
 
 (*try to reconstruct the record name type abbreviation from
   the (nested) extension types*)
 fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =

     val midx = maxidx_of_typ T;
     val varifyT = varifyT midx;
 
     fun mk_type_abbr subst name args =
       let val abbrT = Type (name, map (varifyT o TFree) args)
-      in Syntax_Phases.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
+      in Syntax_Phases.term_of_typ ctxt (Envir.norm_type subst abbrT) end;
 
     fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   in
     if ! print_type_abbr then
       (case last_extT T of