src/HOL/Tools/Datatype/datatype_data.ML

     let
       val thy = ProofContext.theory_of ctxt;
       val (vs, cos) = the_spec thy dtco;
       val ty = Type (dtco, map TFree vs);
       val pretty_typ_bracket =
-        Syntax.pretty_typ (Config.put Syntax.pretty_priority (Syntax.max_pri + 1) ctxt);
+        Syntax.pretty_typ (Config.put pretty_priority (Syntax.max_pri + 1) ctxt);
       fun pretty_constr (co, tys) =
         Pretty.block (Pretty.breaks
           (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
             map pretty_typ_bracket tys));
       val pretty_datatype =