# HG changeset patch
# User haftmann
# Date 1743335406 -7200
# Node ID ceb4f33d30736de7ac6f58d8941c1db756511c70
# Parent  3f875966c3e1f05f3c8529acfbc9d29c2e80ca10
tuned namespace organisation

diff -r 3f875966c3e1 -r ceb4f33d3073 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Mar 30 13:50:06 2025 +0200
+++ b/src/HOL/List.thy	Sun Mar 30 13:50:06 2025 +0200
@@ -8156,7 +8156,7 @@
 fun print_list (target_fxy, target_cons) pr fxy t1 t2 =
   Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
     pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
-    Code_Printer.str target_cons,
+    Pretty.str target_cons,
     pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
   );
 
diff -r 3f875966c3e1 -r ceb4f33d3073 src/HOL/Tools/literal.ML
--- a/src/HOL/Tools/literal.ML	Sun Mar 30 13:50:06 2025 +0200
+++ b/src/HOL/Tools/literal.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -103,7 +103,7 @@
   let
     fun pretty literals _ thm _ _ [(b0, _), (b1, _), (b2, _), (b3, _), (b4, _), (b5, _), (b6, _), (t, _)] =
       case implode_literal b0 b1 b2 b3 b4 b5 b6 t of
-        SOME s => (Code_Printer.str o Code_Printer.literal_string literals) s
+        SOME s => (Pretty.str o Code_Printer.literal_string literals) s
       | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
   in
     thy
diff -r 3f875966c3e1 -r ceb4f33d3073 src/HOL/Tools/numeral.ML
--- a/src/HOL/Tools/numeral.ML	Sun Mar 30 13:50:06 2025 +0200
+++ b/src/HOL/Tools/numeral.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -104,7 +104,7 @@
   let
     fun pretty literals _ thm _ _ [(t, _)] =
       case dest_num_code t of
-        SOME n => (Code_Printer.str o print literals o preproc) n
+        SOME n => (Pretty.str o print literals o preproc) n
       | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
   in
     thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
diff -r 3f875966c3e1 -r ceb4f33d3073 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_haskell.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -51,20 +51,20 @@
       | SOME class => class;
     fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
      of [] => []
-      | constraints => enum "," "(" ")" (
+      | constraints => Pretty.enum "," "(" ")" (
           map (fn (v, class) =>
-            str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
-          @@ str " => ";
+            Pretty.str (class_name class ^ " " ^ lookup_var tyvars v)) constraints)
+          @@ Pretty.str " => ";
     fun print_typforall tyvars vs = case map fst vs
      of [] => []
-      | vnames => str "forall " :: Pretty.breaks
-          (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
+      | vnames => Pretty.str "forall " :: Pretty.breaks
+          (map (Pretty.str o lookup_var tyvars) vnames) @ Pretty.str "." @@ Pretty.brk 1;
     fun print_tyco_expr tyvars fxy (tyco, tys) =
-      brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
+      brackify fxy (Pretty.str tyco :: map (print_typ tyvars BR) tys)
     and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
          of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys)
           | SOME (_, print) => print (print_typ tyvars) fxy tys)
-      | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
+      | print_typ tyvars fxy (ITyVar v) = (Pretty.str o lookup_var tyvars) v;
     fun print_typdecl tyvars (tyco, vs) =
       print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
     fun print_typscheme tyvars (vs, ty) =
@@ -80,14 +80,14 @@
                   print_term tyvars some_thm vars BR t2
                 ])
       | print_term tyvars some_thm vars fxy (IVar NONE) =
-          str "_"
+          Pretty.str "_"
       | print_term tyvars some_thm vars fxy (IVar (SOME v)) =
-          (str o lookup_var vars) v
+          (Pretty.str o lookup_var vars) v
       | print_term tyvars some_thm vars fxy (t as _ `|=> _) =
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
             val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
-          in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
+          in brackets (Pretty.str "\\" :: ps @ Pretty.str "->" @@ print_term tyvars some_thm vars' NOBR t') end
       | print_term tyvars some_thm vars fxy (ICase case_expr) =
           (case Code_Thingol.unfold_const_app (#primitive case_expr)
            of SOME (app as ({ sym = Constant const, ... }, _)) =>
@@ -99,42 +99,42 @@
       let
         val printed_const =
           case annotation of
-            SOME ty => brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
-          | NONE => (str o deresolve) sym
+            SOME ty => brackets [(Pretty.str o deresolve) sym, Pretty.str "::", print_typ tyvars NOBR ty]
+          | NONE => (Pretty.str o deresolve) sym
       in 
         printed_const :: map (print_term tyvars some_thm vars BR) ts
       end
     and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
     and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
     and print_case tyvars some_thm vars fxy { clauses = [], ... } =
-          (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
+          (brackify fxy o Pretty.breaks o map Pretty.str) ["error", "\"empty case\""]
       | print_case tyvars some_thm vars fxy (case_expr as { clauses = [(IVar _, _)], ... }) =
           let
             val (vs, body) = Code_Thingol.unfold_let_no_pat (ICase case_expr);
             fun print_assignment ((some_v, _), t) vars =
               vars
               |> print_bind tyvars some_thm BR (IVar some_v)
-              |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
+              |>> (fn p => semicolon [p, Pretty.str "=", print_term tyvars some_thm vars NOBR t])
             val (ps, vars') = fold_map print_assignment vs vars;
-          in brackify_block fxy (str "let {")
+          in brackify_block fxy (Pretty.str "let {")
             ps
-            (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
+            (concat [Pretty.str "}", Pretty.str "in", print_term tyvars some_thm vars' NOBR body])
           end
       | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
           let
             fun print_select (pat, body) =
               let
                 val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
-              in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
+              in semicolon [p, Pretty.str "->", print_term tyvars some_thm vars' NOBR body] end;
           in Pretty.block_enclose
-            (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
+            (concat [Pretty.str "(case", print_term tyvars some_thm vars NOBR t, Pretty.str "of", Pretty.str "{"], Pretty.str "})")
             (map print_select clauses)
           end;
     fun print_stmt (Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
             fun print_err n =
-              (semicolon o map str) (
+              (semicolon o map Pretty.str) (
                 deresolve_const const
                 :: replicate n "_"
                 @ "="
@@ -149,16 +149,16 @@
                   |> intro_vars (build (fold Code_Thingol.add_varnames ts));
               in
                 semicolon (
-                  (str o deresolve_const) const
+                  (Pretty.str o deresolve_const) const
                   :: map (print_term tyvars some_thm vars BR) ts
-                  @ str "="
+                  @ Pretty.str "="
                   @@ print_term tyvars some_thm vars NOBR t
                 )
               end;
           in
             Pretty.chunks (
               semicolon [
-                (str o suffix " ::" o deresolve_const) const,
+                (Pretty.str o suffix " ::" o deresolve_const) const,
                 print_typscheme tyvars (vs, ty)
               ]
               :: (case filter (snd o snd) raw_eqs
@@ -171,7 +171,7 @@
             val tyvars = intro_vars vs reserved;
           in
             semicolon [
-              str "data",
+              Pretty.str "data",
               print_typdecl tyvars (deresolve_tyco tyco, vs)
             ]
           end
@@ -180,12 +180,12 @@
             val tyvars = intro_vars vs reserved;
           in
             semicolon (
-              str "newtype"
+              Pretty.str "newtype"
               :: print_typdecl tyvars (deresolve_tyco tyco, vs)
-              :: str "="
-              :: (str o deresolve_const) co
+              :: Pretty.str "="
+              :: (Pretty.str o deresolve_const) co
               :: print_typ tyvars BR ty
-              :: (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else [])
+              :: (if deriving_show tyco then [Pretty.str "deriving (Prelude.Read, Prelude.Show)"] else [])
             )
           end
       | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
@@ -193,17 +193,17 @@
             val tyvars = intro_vars vs reserved;
             fun print_co ((co, _), tys) =
               concat (
-                (str o deresolve_const) co
+                (Pretty.str o deresolve_const) co
                 :: map (print_typ tyvars BR) tys
               )
           in
             semicolon (
-              str "data"
+              Pretty.str "data"
               :: print_typdecl tyvars (deresolve_tyco tyco, vs)
-              :: str "="
+              :: Pretty.str "="
               :: print_co co
-              :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
-              @ (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else [])
+              :: map ((fn p => Pretty.block [Pretty.str "| ", p]) o print_co) cos
+              @ (if deriving_show tyco then [Pretty.str "deriving (Prelude.Read, Prelude.Show)"] else [])
             )
           end
       | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
@@ -211,19 +211,19 @@
             val tyvars = intro_vars [v] reserved;
             fun print_classparam (classparam, ty) =
               semicolon [
-                (str o deresolve_const) classparam,
-                str "::",
+                (Pretty.str o deresolve_const) classparam,
+                Pretty.str "::",
                 print_typ tyvars NOBR ty
               ]
           in
             Pretty.block_enclose (
               Pretty.block [
-                str "class ",
+                Pretty.str "class ",
                 Pretty.block (print_typcontext tyvars [(v, map snd classrels)]),
-                str (deresolve_class class ^ " " ^ lookup_var tyvars v),
-                str " where {"
+                Pretty.str (deresolve_class class ^ " " ^ lookup_var tyvars v),
+                Pretty.str " where {"
               ],
-              str "};"
+              Pretty.str "};"
             ) (map print_classparam classparams)
           end
       | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
@@ -232,13 +232,13 @@
             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
               case const_syntax classparam of
                 NONE => semicolon [
-                    (str o Long_Name.base_name o deresolve_const) classparam,
-                    str "=",
+                    (Pretty.str o Long_Name.base_name o deresolve_const) classparam,
+                    Pretty.str "=",
                     print_app tyvars (SOME thm) reserved NOBR (const, [])
                   ]
               | SOME (_, Code_Printer.Plain_printer s) => semicolon [
-                    (str o Long_Name.base_name) s,
-                    str "=",
+                    (Pretty.str o Long_Name.base_name) s,
+                    Pretty.str "=",
                     print_app tyvars (SOME thm) reserved NOBR (const, [])
                   ]
               | SOME (wanted, Code_Printer.Complex_printer _) =>
@@ -258,20 +258,20 @@
                   in
                     semicolon [
                       print_term tyvars (SOME thm) vars NOBR lhs,
-                      str "=",
+                      Pretty.str "=",
                       print_term tyvars (SOME thm) vars NOBR rhs
                     ]
                   end;
           in
             Pretty.block_enclose (
               Pretty.block [
-                str "instance ",
+                Pretty.str "instance ",
                 Pretty.block (print_typcontext tyvars vs),
-                str (class_name class ^ " "),
+                Pretty.str (class_name class ^ " "),
                 print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
-                str " where {"
+                Pretty.str " where {"
               ],
-              str "};"
+              Pretty.str "};"
             ) (map print_classparam_instance inst_params)
           end;
   in print_stmt end;
@@ -368,31 +368,31 @@
     fun print_module_frame module_name header exports ps =
       (module_names module_name, Pretty.chunks2 (
         header
-        @ concat [str "module",
+        @ concat [Pretty.str "module",
           case exports of
-            SOME ps => Pretty.block [str module_name, enclose "(" ")" (commas ps)]
-          | NONE => str module_name,
-          str "where {"
+            SOME ps => Pretty.block [Pretty.str module_name, Pretty.enclose "(" ")" (Pretty.commas ps)]
+          | NONE => Pretty.str module_name,
+          Pretty.str "where {"
         ]
         :: ps
-        @| str "}"
+        @| Pretty.str "}"
       ));
     fun print_qualified_import module_name =
-      semicolon [str "import qualified", str module_name];
+      semicolon [Pretty.str "import qualified", Pretty.str module_name];
     val import_common_ps =
-      enclose "import Prelude (" ");" (commas (map str
-        (map (Library.enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
-          @ map (fn (tyco, constrs) => (enclose (tyco ^ "(") ")" o commas o map str) constrs) prelude_import_unqualified_constr))
-      :: enclose "import Data.Bits (" ");" (commas
-        (map (str o Library.enclose "(" ")") data_bits_import_operators))
+      Pretty.enclose "import Prelude (" ");" (Pretty.commas (map Pretty.str
+        (map (enclose "(" ")") prelude_import_operators @ prelude_import_unqualified)
+          @ map (fn (tyco, constrs) => (Pretty.enclose (tyco ^ "(") ")" o Pretty.commas o map Pretty.str) constrs) prelude_import_unqualified_constr))
+      :: Pretty.enclose "import Data.Bits (" ");" (Pretty.commas
+        (map (Pretty.str o enclose "(" ")") data_bits_import_operators))
       :: print_qualified_import "Prelude"
       :: print_qualified_import "Data.Bits"
       :: map (print_qualified_import o fst) includes;
     fun print_module module_name (gr, imports) =
       let
         val deresolve = deresolver module_name;
-        val deresolve_import = SOME o str o deresolve;
-        val deresolve_import_attached = SOME o str o suffix "(..)" o deresolve;
+        val deresolve_import = SOME o Pretty.str o deresolve;
+        val deresolve_import_attached = SOME o Pretty.str o suffix "(..)" o deresolve;
         fun print_import (sym, (_, Code_Thingol.Fun _)) = deresolve_import sym
           | print_import (sym, (Code_Namespace.Public, Code_Thingol.Datatype _)) = deresolve_import_attached sym
           | print_import (sym, (Code_Namespace.Opaque, Code_Thingol.Datatype _)) = deresolve_import sym
@@ -409,7 +409,7 @@
           |> split_list
           |> apfst (map_filter I);
       in
-        print_module_frame module_name [str language_pragma] (SOME export_ps)
+        print_module_frame module_name [Pretty.str language_pragma] (SOME export_ps)
           ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
       end;
 
@@ -430,7 +430,7 @@
 val literals = Literals {
   literal_string = print_haskell_string,
   literal_numeral = print_numeral "Integer",
-  literal_list = enum "," "[" "]",
+  literal_list = Pretty.enum "," "[" "]",
   infix_cons = (5, ":")
 };
 
@@ -455,22 +455,22 @@
           (semicolon [print_term vars NOBR t], vars)
       | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
           |> print_bind NOBR bind
-          |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t])
+          |>> (fn p => semicolon [p, Pretty.str "<-", print_term vars NOBR t])
       | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
           |> print_bind NOBR bind
-          |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
+          |>> (fn p => semicolon [Pretty.str "let", Pretty.str "{", p, Pretty.str "=", print_term vars NOBR t, Pretty.str "}"]);
     fun pretty _ print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
      of SOME (bind, t') => let
           val (binds, t'') = implode_monad t'
           val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
             (bind :: binds) vars;
         in
-          brackify_block fxy (str "do { ")
+          brackify_block fxy (Pretty.str "do { ")
             (ps @| print_term vars' NOBR t'')
-            (str " }")
+            (Pretty.str " }")
         end
       | NONE => brackify_infix (1, L) fxy
-          (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
+          (print_term vars (INFX (1, L)) t1, Pretty.str ">>=", print_term vars (INFX (1, X)) t2)
   in (2, pretty) end;
 
 fun add_monad target' raw_c_bind thy =
@@ -499,7 +499,7 @@
     [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (
         print_typ (INFX (1, X)) ty1,
-        str "->",
+        Pretty.str "->",
         print_typ (INFX (1, R)) ty2
       )))]))
   #> fold (Code_Target.add_reserved target) [
diff -r 3f875966c3e1 -r ceb4f33d3073 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_ml.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -42,11 +42,11 @@
 
 fun print_product _ [] = NONE
   | print_product print [x] = SOME (print x)
-  | print_product print xs = (SOME o enum " *" "" "") (map print xs);
+  | print_product print xs = (SOME o Pretty.enum " *" "" "") (map print xs);
 
 fun tuplify _ _ [] = NONE
   | tuplify print fxy [x] = SOME (print fxy x)
-  | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
+  | tuplify print _ xs = SOME (Pretty.enum "," "(" ")" (map (print NOBR) xs));
 
 
 (** SML serializer **)
@@ -65,33 +65,33 @@
     val deresolve_const = deresolve o Constant;
     val deresolve_classrel = deresolve o Class_Relation;
     val deresolve_inst = deresolve o Class_Instance;
-    fun print_tyco_expr (sym, []) = (str o deresolve) sym
+    fun print_tyco_expr (sym, []) = (Pretty.str o deresolve) sym
       | print_tyco_expr (sym, [ty]) =
-          concat [print_typ BR ty, (str o deresolve) sym]
+          concat [print_typ BR ty, (Pretty.str o deresolve) sym]
       | print_tyco_expr (sym, tys) =
-          concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
+          concat [Pretty.enum "," "(" ")" (map (print_typ BR) tys), (Pretty.str o deresolve) sym]
     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
          of NONE => print_tyco_expr (Type_Constructor tyco, tys)
           | SOME (_, print) => print print_typ fxy tys)
-      | print_typ fxy (ITyVar v) = str ("'" ^ v);
+      | print_typ fxy (ITyVar v) = Pretty.str ("'" ^ v);
     fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
-    fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
+    fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" ""
       (map_filter (fn (v, sort) =>
         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
     fun print_classrels fxy [] ps = brackify fxy ps
-      | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve_classrel) classrel, brackify BR ps]
+      | print_classrels fxy [classrel] ps = brackify fxy [(Pretty.str o deresolve_classrel) classrel, brackify BR ps]
       | print_classrels fxy classrels ps =
-          brackify fxy [enum " o" "(" ")" (map (str o deresolve_classrel) classrels), brackify BR ps]
+          brackify fxy [Pretty.enum " o" "(" ")" (map (Pretty.str o deresolve_classrel) classrels), brackify BR ps]
     fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
       print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
-          ((str o deresolve_inst) inst ::
-            (if is_pseudo_fun (Class_Instance inst) then [str "()"]
+          ((Pretty.str o deresolve_inst) inst ::
+            (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"]
             else map_filter (print_dicts is_pseudo_fun BR o snd) dss))
       | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) =
-          [str (if length = 1 then Name.enforce_case true var ^ "_"
+          [Pretty.str (if length = 1 then Name.enforce_case true var ^ "_"
             else Name.enforce_case true var ^ string_of_int (index + 1) ^ "_")]
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
@@ -100,9 +100,9 @@
     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
           print_app is_pseudo_fun some_thm vars fxy (const, [])
       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
-          str "_"
+          Pretty.str "_"
       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
-          str (lookup_var vars v)
+          Pretty.str (lookup_var vars v)
       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
            of SOME app => print_app is_pseudo_fun some_thm vars fxy app
@@ -113,7 +113,7 @@
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
             fun print_abs (pat, ty) =
               print_bind is_pseudo_fun some_thm NOBR pat
-              #>> (fn p => concat [str "fn", p, str "=>"]);
+              #>> (fn p => concat [Pretty.str "fn", p, Pretty.str "=>"]);
             val (ps, vars') = fold_map print_abs binds vars;
           in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
       | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
@@ -127,33 +127,33 @@
       if is_constr sym then
         let val wanted = length dom in
           if wanted < 2 orelse length ts = wanted
-          then (str o deresolve) sym
+          then (Pretty.str o deresolve) sym
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)]
         end
       else if is_pseudo_fun sym
-        then (str o deresolve) sym @@ str "()"
-      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
+        then (Pretty.str o deresolve) sym @@ Pretty.str "()"
+      else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
         @ map (print_term is_pseudo_fun some_thm vars BR) ts
     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
       (print_term is_pseudo_fun) const_syntax some_thm vars
     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
     and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
-          (concat o map str) ["raise", "Fail", "\"empty case\""]
+          (concat o map Pretty.str) ["raise", "Fail", "\"empty case\""]
       | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
             fun print_match ((pat, _), t) vars =
               vars
               |> print_bind is_pseudo_fun some_thm NOBR pat
-              |>> (fn p => semicolon [str "val", p, str "=",
+              |>> (fn p => semicolon [Pretty.str "val", p, Pretty.str "=",
                     print_term is_pseudo_fun some_thm vars NOBR t])
             val (ps, vars') = fold_map print_match binds vars;
           in
             Pretty.chunks [
-              Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps],
-              Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],
-              str "end"
+              Pretty.block [Pretty.str "let", Pretty.fbrk, Pretty.chunks ps],
+              Pretty.block [Pretty.str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],
+              Pretty.str "end"
             ]
           end
       | print_case is_pseudo_fun some_thm vars fxy { term = t, typ = ty, clauses = clause :: clauses, ... } =
@@ -162,29 +162,29 @@
               let
                 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
               in
-                concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]
+                concat [Pretty.str delim, p, Pretty.str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]
               end;
           in
             brackets (
-              str "case"
+              Pretty.str "case"
               :: print_term is_pseudo_fun some_thm vars NOBR t
               :: print_select "of" clause
               :: map (print_select "|") clauses
             )
           end;
     fun print_val_decl print_typscheme (sym, typscheme) = concat
-      [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
+      [Pretty.str "val", Pretty.str (deresolve sym), Pretty.str ":", print_typscheme typscheme];
     fun print_datatype_decl definer (tyco, (vs, cos)) =
       let
-        fun print_co ((co, _), []) = str (deresolve_const co)
-          | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
-              enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
+        fun print_co ((co, _), []) = Pretty.str (deresolve_const co)
+          | print_co ((co, _), tys) = concat [Pretty.str (deresolve_const co), Pretty.str "of",
+              Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
       in
         concat (
-          str definer
+          Pretty.str definer
           :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
-          :: str "="
-          :: separate (str "|") (map print_co cos)
+          :: Pretty.str "="
+          :: separate (Pretty.str "|") (map print_co cos)
         )
       end;
     fun print_def is_pseudo_fun needs_typ definer
@@ -197,15 +197,15 @@
                        deresolve (t :: ts)
                   |> intro_vars (build (fold Code_Thingol.add_varnames ts));
                 val prolog = if needs_typ then
-                  concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
-                    else (concat o map str) [definer, deresolve_const const];
+                  concat [Pretty.str definer, (Pretty.str o deresolve_const) const, Pretty.str ":", print_typ NOBR ty]
+                    else (concat o map Pretty.str) [definer, deresolve_const const];
               in
                 concat (
                   prolog
-                  :: (if is_pseudo_fun (Constant const) then [str "()"]
+                  :: (if is_pseudo_fun (Constant const) then [Pretty.str "()"]
                       else print_dict_args vs
                         @ map (print_term is_pseudo_fun some_thm vars BR) ts)
-                  @ str "="
+                  @ Pretty.str "="
                   @@ print_term is_pseudo_fun some_thm vars NOBR t
                 )
               end
@@ -223,35 +223,35 @@
           let
             fun print_super_instance (super_class, x) =
               concat [
-                (str o Long_Name.base_name o deresolve_classrel) (class, super_class),
-                str "=",
+                (Pretty.str o Long_Name.base_name o deresolve_classrel) (class, super_class),
+                Pretty.str "=",
                 print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), x)))
               ];
             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
               concat [
-                (str o Long_Name.base_name o deresolve_const) classparam,
-                str "=",
+                (Pretty.str o Long_Name.base_name o deresolve_const) classparam,
+                Pretty.str "=",
                 print_app (K false) (SOME thm) reserved NOBR (const, [])
               ];
           in pair
             (print_val_decl print_dicttypscheme
               (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
             (concat (
-              str definer
-              :: (str o deresolve_inst) inst
-              :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
+              Pretty.str definer
+              :: (Pretty.str o deresolve_inst) inst
+              :: (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"]
                   else print_dict_args vs)
-              @ str "="
-              :: enum "," "{" "}"
+              @ Pretty.str "="
+              :: Pretty.enum "," "{" "}"
                 (map print_super_instance superinsts
                   @ map print_classparam_instance inst_params)
-              :: str ":"
+              :: Pretty.str ":"
               @@ print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
             ))
           end;
     fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
           [print_val_decl print_typscheme (Constant const, vs_ty)]
-          ((semicolon o map str) (
+          ((semicolon o map Pretty.str) (
             (if n = 0 then "val" else "fun")
             :: deresolve_const const
             :: replicate n "_"
@@ -271,11 +271,11 @@
           let
             val print_def' = print_def (member (op =) pseudo_funs) false;
             fun print_pseudo_fun sym = concat [
-                str "val",
-                (str o deresolve) sym,
-                str "=",
-                (str o deresolve) sym,
-                str "();"
+                Pretty.str "val",
+                (Pretty.str o deresolve) sym,
+                Pretty.str "=",
+                (Pretty.str o deresolve) sym,
+                Pretty.str "();"
               ];
             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
               (print_def' "fun" binding :: map (print_def' "and" o snd) exports_bindings);
@@ -290,8 +290,8 @@
             val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
           in
             pair
-            [concat [str "type", ty_p]]
-            (semicolon [str "datatype", ty_p, str "=", str "EMPTY__"])
+            [concat [Pretty.str "type", ty_p]]
+            (semicolon [Pretty.str "datatype", ty_p, Pretty.str "=", Pretty.str "EMPTY__"])
           end
      | print_stmt export (ML_Datas (data :: datas)) = 
           let
@@ -302,15 +302,15 @@
             (if Code_Namespace.is_public export
               then decl_ps
               else map (fn (tyco, (vs, _)) =>
-                concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
+                concat [Pretty.str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
                 (data :: datas))
             (Pretty.chunks (ps @| semicolon [p]))
           end
      | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
           let
-            fun print_field s p = concat [str s, str ":", p];
+            fun print_field s p = concat [Pretty.str s, Pretty.str ":", p];
             fun print_proj s p = semicolon
-              (map str ["val", s, "=", "#" ^ s, ":"] @| p);
+              (map Pretty.str ["val", s, "=", "#" ^ s, ":"] @| p);
             fun print_super_class_decl (classrel as (_, super_class)) =
               print_val_decl print_dicttypscheme
                 (Class_Relation classrel, ([(v, [class])], (super_class, ITyVar v)));
@@ -328,17 +328,17 @@
               print_proj (deresolve_const classparam)
                 (print_typscheme ([(v, [class])], ty));
           in pair
-            (concat [str "type", print_dicttyp (class, ITyVar v)]
+            (concat [Pretty.str "type", print_dicttyp (class, ITyVar v)]
               :: (if Code_Namespace.is_public export
                  then map print_super_class_decl classrels
                    @ map print_classparam_decl classparams
                  else []))
             (Pretty.chunks (
               concat [
-                str "type",
+                Pretty.str "type",
                 print_dicttyp (class, ITyVar v),
-                str "=",
-                enum "," "{" "};" (
+                Pretty.str "=",
+                Pretty.enum "," "{" "};" (
                   map print_super_class_field classrels
                   @ map print_classparam_field classparams
                 )
@@ -352,18 +352,18 @@
 fun print_sml_module name decls body =
   Pretty.chunks2 (
     Pretty.chunks [
-      str ("structure " ^ name ^ " : sig"),
-      (indent 2 o Pretty.chunks) decls,
-      str "end = struct"
+      Pretty.str ("structure " ^ name ^ " : sig"),
+      (Pretty.indent 2 o Pretty.chunks) decls,
+      Pretty.str "end = struct"
     ]
     :: body
-    @| str ("end; (*struct " ^ name ^ "*)")
+    @| Pretty.str ("end; (*struct " ^ name ^ "*)")
   );
 
 val literals_sml = Literals {
   literal_string = print_sml_string,
   literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
-  literal_list = enum "," "[" "]",
+  literal_list = Pretty.enum "," "[" "]",
   infix_cons = (7, "::")
 };
 
@@ -392,32 +392,32 @@
     val deresolve_const = deresolve o Constant;
     val deresolve_classrel = deresolve o Class_Relation;
     val deresolve_inst = deresolve o Class_Instance;
-    fun print_tyco_expr (sym, []) = (str o deresolve) sym
+    fun print_tyco_expr (sym, []) = (Pretty.str o deresolve) sym
       | print_tyco_expr (sym, [ty]) =
-          concat [print_typ BR ty, (str o deresolve) sym]
+          concat [print_typ BR ty, (Pretty.str o deresolve) sym]
       | print_tyco_expr (sym, tys) =
-          concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) sym]
+          concat [Pretty.enum "," "(" ")" (map (print_typ BR) tys), (Pretty.str o deresolve) sym]
     and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
          of NONE => print_tyco_expr (Type_Constructor tyco, tys)
           | SOME (_, print) => print print_typ fxy tys)
-      | print_typ fxy (ITyVar v) = str ("'" ^ v);
+      | print_typ fxy (ITyVar v) = Pretty.str ("'" ^ v);
     fun print_dicttyp (class, ty) = print_tyco_expr (Type_Class class, [ty]);
-    fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
+    fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" ""
       (map_filter (fn (v, sort) =>
         (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
     fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
     fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
     val print_classrels =
-      fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve_classrel) classrel])
+      fold_rev (fn classrel => fn p => Pretty.block [p, Pretty.str ".", (Pretty.str o deresolve_classrel) classrel])
     fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
       print_plain_dict is_pseudo_fun fxy x
       |> print_classrels classrels
     and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
-          brackify BR ((str o deresolve_inst) inst ::
-            (if is_pseudo_fun (Class_Instance inst) then [str "()"]
+          brackify BR ((Pretty.str o deresolve_inst) inst ::
+            (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"]
             else map_filter (print_dicts is_pseudo_fun BR o snd) dss))
       | print_plain_dict is_pseudo_fun fxy (Dict_Var { var, index, length, ... }) =
-          str (if length = 1 then "_" ^ Name.enforce_case true var
+          Pretty.str (if length = 1 then "_" ^ Name.enforce_case true var
             else "_" ^ Name.enforce_case true var ^ string_of_int (index + 1))
     and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
     val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
@@ -426,9 +426,9 @@
     fun print_term is_pseudo_fun some_thm vars fxy (IConst const) =
           print_app is_pseudo_fun some_thm vars fxy (const, [])
       | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
-          str "_"
+          Pretty.str "_"
       | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
-          str (lookup_var vars v)
+          Pretty.str (lookup_var vars v)
       | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
           (case Code_Thingol.unfold_const_app t
            of SOME app => print_app is_pseudo_fun some_thm vars fxy app
@@ -438,7 +438,7 @@
           let
             val (binds, t') = Code_Thingol.unfold_pat_abs t;
             val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
-          in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
+          in brackets (Pretty.str "fun" :: ps @ Pretty.str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
       | print_term is_pseudo_fun some_thm vars fxy (ICase case_expr) =
           (case Code_Thingol.unfold_const_app (#primitive case_expr)
            of SOME (app as ({ sym = Constant const, ... }, _)) =>
@@ -450,19 +450,19 @@
       if is_constr sym then
         let val wanted = length dom in
           if length ts = wanted
-          then (str o deresolve) sym
+          then (Pretty.str o deresolve) sym
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
           else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.saturated_application wanted app)]
         end
       else if is_pseudo_fun sym
-        then (str o deresolve) sym @@ str "()"
-      else (str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
+        then (Pretty.str o deresolve) sym @@ Pretty.str "()"
+      else (Pretty.str o deresolve) sym :: map_filter (print_dicts is_pseudo_fun BR) dicts
         @ map (print_term is_pseudo_fun some_thm vars BR) ts
     and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
       (print_term is_pseudo_fun) const_syntax some_thm vars
     and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
     and print_case is_pseudo_fun some_thm vars fxy { clauses = [], ... } =
-          (concat o map str) ["failwith", "\"empty case\""]
+          (concat o map Pretty.str) ["failwith", "\"empty case\""]
       | print_case is_pseudo_fun some_thm vars fxy (case_expr as { clauses = [_], ... }) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
@@ -470,7 +470,7 @@
               vars
               |> print_bind is_pseudo_fun some_thm NOBR pat
               |>> (fn p => concat
-                  [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
+                  [Pretty.str "let", p, Pretty.str "=", print_term is_pseudo_fun some_thm vars NOBR t, Pretty.str "in"])
             val (ps, vars') = fold_map print_let binds vars;
           in
             brackets [Pretty.chunks ps, print_term is_pseudo_fun some_thm vars' NOBR body]
@@ -480,28 +480,28 @@
             fun print_select delim (pat, body) =
               let
                 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
-              in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
+              in concat [Pretty.str delim, p, Pretty.str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
           in
             brackets (
-              str "match"
+              Pretty.str "match"
               :: print_term is_pseudo_fun some_thm vars NOBR t
               :: print_select "with" clause
               :: map (print_select "|") clauses
             )
           end;
     fun print_val_decl print_typscheme (sym, typscheme) = concat
-      [str "val", str (deresolve sym), str ":", print_typscheme typscheme];
+      [Pretty.str "val", Pretty.str (deresolve sym), Pretty.str ":", print_typscheme typscheme];
     fun print_datatype_decl definer (tyco, (vs, cos)) =
       let
-        fun print_co ((co, _), []) = str (deresolve_const co)
-          | print_co ((co, _), tys) = concat [str (deresolve_const co), str "of",
-              enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
+        fun print_co ((co, _), []) = Pretty.str (deresolve_const co)
+          | print_co ((co, _), tys) = concat [Pretty.str (deresolve_const co), Pretty.str "of",
+              Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)];
       in
         concat (
-          str definer
+          Pretty.str definer
           :: print_tyco_expr (Type_Constructor tyco, map ITyVar vs)
-          :: str "="
-          :: separate (str "|") (map print_co cos)
+          :: Pretty.str "="
+          :: separate (Pretty.str "|") (map print_co cos)
         )
       end;
     fun print_def is_pseudo_fun needs_typ definer
@@ -514,9 +514,9 @@
                       deresolve (t :: ts)
                   |> intro_vars (build (fold Code_Thingol.add_varnames ts));
               in concat [
-                (Pretty.block o commas)
+                (Pretty.block o Pretty.commas)
                   (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
-                str "->",
+                Pretty.str "->",
                 print_term is_pseudo_fun some_thm vars NOBR t
               ] end;
             fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
@@ -527,20 +527,20 @@
                       |> intro_vars (build (fold Code_Thingol.add_varnames ts));
                   in
                     concat (
-                      (if is_pseudo then [str "()"]
+                      (if is_pseudo then [Pretty.str "()"]
                         else map (print_term is_pseudo_fun some_thm vars BR) ts)
-                      @ str "="
+                      @ Pretty.str "="
                       @@ print_term is_pseudo_fun some_thm vars NOBR t
                     )
                   end
               | print_eqns _ ((eq as (([_], _), _)) :: eqs) =
                   Pretty.block (
-                    str "="
+                    Pretty.str "="
                     :: Pretty.brk 1
-                    :: str "function"
+                    :: Pretty.str "function"
                     :: Pretty.brk 1
                     :: print_eqn eq
-                    :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
+                    :: maps (append [Pretty.fbrk, Pretty.str "|", Pretty.brk 1]
                           o single o print_eqn) eqs
                   )
               | print_eqns _ (eqs as eq :: eqs') =
@@ -548,27 +548,27 @@
                     val vars = reserved
                       |> intro_base_names_for (is_none o const_syntax)
                            deresolve (map (snd o fst) eqs)
-                    val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
+                    val dummy_parms = (map Pretty.str o aux_params vars o map (fst o fst)) eqs;
                   in
                     Pretty.block (
                       Pretty.breaks dummy_parms
                       @ Pretty.brk 1
-                      :: str "="
+                      :: Pretty.str "="
                       :: Pretty.brk 1
-                      :: str "match"
+                      :: Pretty.str "match"
                       :: Pretty.brk 1
-                      :: (Pretty.block o commas) dummy_parms
+                      :: (Pretty.block o Pretty.commas) dummy_parms
                       :: Pretty.brk 1
-                      :: str "with"
+                      :: Pretty.str "with"
                       :: Pretty.brk 1
                       :: print_eqn eq
-                      :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
+                      :: maps (append [Pretty.fbrk, Pretty.str "|", Pretty.brk 1]
                            o single o print_eqn) eqs'
                     )
                   end;
             val prolog = if needs_typ then
-              concat [str definer, (str o deresolve_const) const, str ":", print_typ NOBR ty]
-                else (concat o map str) [definer, deresolve_const const];
+              concat [Pretty.str definer, (Pretty.str o deresolve_const) const, Pretty.str ":", print_typ NOBR ty]
+                else (concat o map Pretty.str) [definer, deresolve_const const];
           in pair
             (print_val_decl print_typscheme (Constant const, vs_ty))
             (concat (
@@ -582,36 +582,36 @@
           let
             fun print_super_instance (super_class, dss) =
               concat [
-                (str o deresolve_classrel) (class, super_class),
-                str "=",
+                (Pretty.str o deresolve_classrel) (class, super_class),
+                Pretty.str "=",
                 print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const ((tyco, super_class), dss)))
               ];
             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
               concat [
-                (str o deresolve_const) classparam,
-                str "=",
+                (Pretty.str o deresolve_const) classparam,
+                Pretty.str "=",
                 print_app (K false) (SOME thm) reserved NOBR (const, [])
               ];
           in pair
             (print_val_decl print_dicttypscheme
               (Class_Instance inst, (vs, (class, tyco `%% map (ITyVar o fst) vs))))
             (concat (
-              str definer
-              :: (str o deresolve_inst) inst
-              :: (if is_pseudo_fun (Class_Instance inst) then [str "()"]
+              Pretty.str definer
+              :: (Pretty.str o deresolve_inst) inst
+              :: (if is_pseudo_fun (Class_Instance inst) then [Pretty.str "()"]
                   else print_dict_args vs)
-              @ str "="
+              @ Pretty.str "="
               @@ brackets [
                 enum_default "()" ";" "{" "}" (map print_super_instance superinsts
                   @ map print_classparam_instance inst_params),
-                str ":",
+                Pretty.str ":",
                 print_dicttyp (class, tyco `%% map (ITyVar o fst) vs)
               ]
             ))
           end;
      fun print_stmt _ (ML_Exc (const, (vs_ty, n))) = pair
           [print_val_decl print_typscheme (Constant const, vs_ty)]
-          ((doublesemicolon o map str) (
+          ((doublesemicolon o map Pretty.str) (
             "let"
             :: deresolve_const const
             :: replicate n "_"
@@ -630,11 +630,11 @@
           let
             val print_def' = print_def (member (op =) pseudo_funs) false;
             fun print_pseudo_fun sym = concat [
-                str "let",
-                (str o deresolve) sym,
-                str "=",
-                (str o deresolve) sym,
-                str "();;"
+                Pretty.str "let",
+                (Pretty.str o deresolve) sym,
+                Pretty.str "=",
+                (Pretty.str o deresolve) sym,
+                Pretty.str "();;"
               ];
             val (sig_ps, (ps, p)) = (apsnd split_last o split_list)
               (print_def' "let rec" binding :: map (print_def' "and" o snd) exports_bindings);
@@ -649,8 +649,8 @@
             val ty_p = print_tyco_expr (Type_Constructor tyco, map ITyVar vs);
           in
             pair
-            [concat [str "type", ty_p]]
-            (doublesemicolon [str "type", ty_p, str "=", str "EMPTY__"])
+            [concat [Pretty.str "type", ty_p]]
+            (doublesemicolon [Pretty.str "type", ty_p, Pretty.str "=", Pretty.str "EMPTY__"])
           end
      | print_stmt export (ML_Datas (data :: datas)) = 
           let
@@ -661,13 +661,13 @@
             (if Code_Namespace.is_public export
               then decl_ps
               else map (fn (tyco, (vs, _)) =>
-                concat [str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
+                concat [Pretty.str "type", print_tyco_expr (Type_Constructor tyco, map ITyVar vs)])
                 (data :: datas))
             (Pretty.chunks (ps @| doublesemicolon [p]))
           end
      | print_stmt export (ML_Class (class, (v, (classrels, classparams)))) =
           let
-            fun print_field s p = concat [str s, str ":", p];
+            fun print_field s p = concat [Pretty.str s, Pretty.str ":", p];
             fun print_super_class_field (classrel as (_, super_class)) =
               print_field (deresolve_classrel classrel) (print_dicttyp (super_class, ITyVar v));
             fun print_classparam_decl (classparam, ty) =
@@ -677,12 +677,12 @@
               print_field (deresolve_const classparam) (print_typ NOBR ty);
             val w = "_" ^ Name.enforce_case true v;
             fun print_classparam_proj (classparam, _) =
-              (concat o map str) ["let", deresolve_const classparam, w, "=",
+              (concat o map Pretty.str) ["let", deresolve_const classparam, w, "=",
                 w ^ "." ^ deresolve_const classparam ^ ";;"];
             val type_decl_p = concat [
-                str "type",
+                Pretty.str "type",
                 print_dicttyp (class, ITyVar v),
-                str "=",
+                Pretty.str "=",
                 enum_default "unit" ";" "{" "}" (
                   map print_super_class_field classrels
                   @ map print_classparam_field classparams
@@ -693,7 +693,7 @@
               then type_decl_p :: map print_classparam_decl classparams
               else if null classrels andalso null classparams
               then [type_decl_p] (*work around weakness in export calculation*)
-              else [concat [str "type", print_dicttyp (class, ITyVar v)]])
+              else [concat [Pretty.str "type", print_dicttyp (class, ITyVar v)]])
             (Pretty.chunks (
               doublesemicolon [type_decl_p]
               :: map print_classparam_proj classparams
@@ -704,12 +704,12 @@
 fun print_ocaml_module name decls body =
   Pretty.chunks2 (
     Pretty.chunks [
-      str ("module " ^ name ^ " : sig"),
-      (indent 2 o Pretty.chunks) decls,
-      str "end = struct"
+      Pretty.str ("module " ^ name ^ " : sig"),
+      (Pretty.indent 2 o Pretty.chunks) decls,
+      Pretty.str "end = struct"
     ]
     :: body
-    @| str ("end;; (*struct " ^ name ^ "*)")
+    @| Pretty.str ("end;; (*struct " ^ name ^ "*)")
   );
 
 val literals_ocaml = let
@@ -721,7 +721,7 @@
 in Literals {
   literal_string = print_ocaml_string,
   literal_numeral = numeral_ocaml,
-  literal_list = enum ";" "[" "]",
+  literal_list = Pretty.enum ";" "[" "]",
   infix_cons = (6, "::")
 } end;
 
@@ -868,7 +868,7 @@
 fun fun_syntax print_typ fxy [ty1, ty2] =
   brackify_infix (1, R) fxy (
     print_typ (INFX (1, X)) ty1,
-    str "->",
+    Pretty.str "->",
     print_typ (INFX (1, R)) ty2
   );
 
diff -r 3f875966c3e1 -r ceb4f33d3073 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_printer.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -15,16 +15,11 @@
 
   val @@ : 'a * 'a -> 'a list
   val @| : 'a list * 'a -> 'a list
-  val str: string -> Pretty.T
   val concat: Pretty.T list -> Pretty.T
   val brackets: Pretty.T list -> Pretty.T
-  val enclose: string -> string -> Pretty.T list -> Pretty.T
-  val commas: Pretty.T list -> Pretty.T list
-  val enum: string -> string -> string -> Pretty.T list -> Pretty.T
   val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
   val semicolon: Pretty.T list -> Pretty.T
   val doublesemicolon: Pretty.T list -> Pretty.T
-  val indent: int -> Pretty.T -> Pretty.T
   val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
   val format: Code_Symbol.T list -> int -> Pretty.T -> Bytes.T
 
@@ -121,17 +116,13 @@
 infixr 5 @|;
 fun x @@ y = [x, y];
 fun xs @| y = xs @ [y];
-val str = Pretty.str;
 val concat = Pretty.block o Pretty.breaks;
 val commas = Pretty.commas;
-val enclose = Pretty.enclose;
-val brackets = enclose "(" ")" o Pretty.breaks;
-val enum = Pretty.enum;
-fun enum_default default sep l r [] = str default
-  | enum_default default sep l r xs = enum sep l r xs;
-fun semicolon ps = Pretty.block [concat ps, str ";"];
-fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
-val indent = Pretty.indent;
+val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
+fun enum_default default sep l r [] = Pretty.str default
+  | enum_default default sep l r xs = Pretty.enum sep l r xs;
+fun semicolon ps = Pretty.block [concat ps, Pretty.str ";"];
+fun doublesemicolon ps = Pretty.block [concat ps, Pretty.str ";;"];
 
 fun markup_stmt sym =
   Pretty.mark (Markup.code_presentationN, [(Markup.stmt_nameN, Code_Symbol.marker sym)]);
@@ -251,34 +242,34 @@
   | fixity _ _ = true;
 
 fun gen_brackify _ [p] = p
-  | gen_brackify true (ps as _::_) = enclose "(" ")" ps
+  | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
   | gen_brackify false (ps as _::_) = Pretty.block ps;
 
 fun brackify fxy_ctxt =
   gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
 
 fun brackify_infix infx fxy_ctxt (l, m, r) =
-  gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r];
+  gen_brackify (fixity (INFX infx) fxy_ctxt) [l, Pretty.str " ", m, Pretty.brk 1, r];
 
 fun brackify_block fxy_ctxt p1 ps p2 =
   let val p = Pretty.block_enclose (p1, p2) ps
   in if fixity BR fxy_ctxt
-    then enclose "(" ")" [p]
+    then Pretty.enclose "(" ")" [p]
     else p
   end;
 
 fun gen_applify strict opn cls f fxy_ctxt p [] =
       if strict
-      then gen_brackify (fixity BR fxy_ctxt) [p, str (opn ^ cls)]
+      then gen_brackify (fixity BR fxy_ctxt) [p, Pretty.str (opn ^ cls)]
       else p
   | gen_applify strict opn cls f fxy_ctxt p ps =
-      gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps));
+      gen_brackify (fixity BR fxy_ctxt) (p @@ Pretty.enum "," opn cls (map f ps));
 
 fun applify opn = gen_applify false opn;
 
 fun tuplify _ _ [] = NONE
   | tuplify print fxy [x] = SOME (print fxy x)
-  | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
+  | tuplify print _ xs = SOME (Pretty.enum "," "(" ")" (map (print NOBR) xs));
 
 
 (* generic syntax *)
@@ -337,7 +328,7 @@
     Constant name => (case const_syntax name of
       NONE => brackify fxy (print_app_expr some_thm vars app)
     | SOME (_, Plain_printer s) =>
-        brackify fxy (str s :: map (print_term some_thm vars BR) ts)
+        brackify fxy (Pretty.str s :: map (print_term some_thm vars BR) ts)
     | SOME (wanted, Complex_printer print) =>
         let
           val ((vs_tys, (ts1, rty)), ts2) =
@@ -382,7 +373,7 @@
       | fillin print (Arg fxy :: mfx) (a :: args) =
           (print fxy o prep_arg) a :: fillin print mfx args
       | fillin print (String s :: mfx) args =
-          str s :: fillin print mfx args
+          Pretty.str s :: fillin print mfx args
       | fillin print (Break :: mfx) args =
           Pretty.brk 1 :: fillin print mfx args;
   in
@@ -430,7 +421,7 @@
       of_printer (printer_of_mixfix prep_arg (fixity, mfx));
 
 fun parse_tyco_syntax x =
-  (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I) x;
+  (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o Pretty.str) s)) I I) x;
 
 val parse_const_syntax =
   parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst;
diff -r 3f875966c3e1 -r ceb4f33d3073 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_runtime.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -55,7 +55,7 @@
 val _ = Theory.setup
   (Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)])
   #> Code_Target.set_printings (Type_Constructor (\<^type_name>\<open>prop\<close>,
-    [(target, SOME (0, (K o K o K) (Code_Printer.str truthN)))]))
+    [(target, SOME (0, (K o K o K) (Pretty.str truthN)))]))
   #> Code_Target.set_printings (Constant (\<^const_name>\<open>Code_Generator.holds\<close>,
     [(target, SOME (Code_Printer.plain_const_syntax HoldsN))]))
   #> Code_Target.add_reserved target thisN
@@ -685,7 +685,7 @@
       | pr pr' _ [ty] =
           Code_Printer.concat [pr' Code_Printer.BR ty, tyco']
       | pr pr' _ tys =
-          Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
+          Code_Printer.concat [Pretty.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco']
   in
     thy
     |> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))]))
@@ -709,9 +709,9 @@
       thy
       |> Code_Target.add_reserved target module_name
       |> Context.theory_map (compile_ML true code)
-      |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
-      |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
-      |> fold (add_eval_const o apsnd Code_Printer.str) const_map
+      |> fold (add_eval_tyco o apsnd Pretty.str) tyco_map
+      |> fold (add_eval_constr o apsnd Pretty.str) constr_map
+      |> fold (add_eval_const o apsnd Pretty.str) const_map
   | process_reflection (code, _) _ (SOME binding) thy =
       let
         val code_binding = Path.map_binding Code_Target.code_path binding;
@@ -856,7 +856,7 @@
   |> Specification.axiomatization [(b, SOME T, NoSyn)] [] [] []
   |-> (fn ([Const (const, _)], _) =>
     Code_Target.set_printings (Constant (const,
-      [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))]))
+      [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Pretty.str) ml_name)))]))
   #> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [const] target Code_Target.generatedN NONE []));
 
 fun process_file filepath (definienda, thy) =
diff -r 3f875966c3e1 -r ceb4f33d3073 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_scala.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -57,29 +57,29 @@
     fun lookup_tyvar tyvars = lookup_var tyvars o Name.enforce_case true;
     fun intro_tyvars vs = intro_vars (map (Name.enforce_case true o fst) vs);
     fun print_tyco_expr tyvars fxy (sym, tys) = applify "[" "]"
-          (print_typ tyvars NOBR) fxy ((str o deresolve) sym) tys
+          (print_typ tyvars NOBR) fxy ((Pretty.str o deresolve) sym) tys
     and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
          of NONE => print_tyco_expr tyvars fxy (Type_Constructor tyco, tys)
           | SOME (_, print) => print (print_typ tyvars) fxy tys)
-      | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
+      | print_typ tyvars fxy (ITyVar v) = (Pretty.str o lookup_tyvar tyvars) v;
     fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (Type_Class class, [ty]);
     fun print_tupled_typ tyvars ([], ty) =
           print_typ tyvars NOBR ty
       | print_tupled_typ tyvars ([ty1], ty2) =
-          concat [print_typ tyvars BR ty1, str "=>", print_typ tyvars NOBR ty2]
+          concat [print_typ tyvars BR ty1, Pretty.str "=>", print_typ tyvars NOBR ty2]
       | print_tupled_typ tyvars (tys, ty) =
-          concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
-            str "=>", print_typ tyvars NOBR ty];
-    fun constraint p1 p2 = Pretty.block [p1, str " : ", p2];
-    fun print_var vars NONE = str "_"
-      | print_var vars (SOME v) = (str o lookup_var vars) v;
+          concat [Pretty.enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
+            Pretty.str "=>", print_typ tyvars NOBR ty];
+    fun constraint p1 p2 = Pretty.block [p1, Pretty.str " : ", p2];
+    fun print_var vars NONE = Pretty.str "_"
+      | print_var vars (SOME v) = (Pretty.str o lookup_var vars) v;
     fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d
     and applify_plain_dict tyvars (Dict_Const (inst, dss)) =
-          applify_dictss tyvars ((str o deresolve o Class_Instance) inst) (map snd dss)
+          applify_dictss tyvars ((Pretty.str o deresolve o Class_Instance) inst) (map snd dss)
       | applify_plain_dict tyvars (Dict_Var { var, class, ... }) =
-          Pretty.block [str "implicitly",
-            enclose "[" "]" [Pretty.block [(str o deresolve_class) class,
-              enclose "[" "]" [(str o lookup_tyvar tyvars) var]]]]
+          Pretty.block [Pretty.str "implicitly",
+            Pretty.enclose "[" "]" [Pretty.block [(Pretty.str o deresolve_class) class,
+              Pretty.enclose "[" "]" [(Pretty.str o lookup_tyvar tyvars) var]]]]
     and applify_dictss tyvars p dss =
       applify "(" ")" (applify_dict tyvars) NOBR p (flat dss)
     fun print_term tyvars is_pat some_thm vars fxy (IConst const) =
@@ -110,8 +110,8 @@
              val vars' = intro_vars (the_list some_v) vars;
            in
              (concat [
-               enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)],
-               str "=>"
+               Pretty.enclose "(" ")" [constraint (print_var vars' some_v) (print_typ tyvars NOBR ty)],
+               Pretty.str "=>"
              ], vars')
            end
     and print_app tyvars is_pat some_thm vars fxy
@@ -131,12 +131,12 @@
               (gen_applify (is_constr sym) "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
-                  NOBR ((str o deresolve) sym) typargs') ts) dicts)
+                  NOBR ((Pretty.str o deresolve) sym) typargs') ts) dicts)
           | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify_dicts
               (applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
-                  NOBR (str s) typargs') ts) dicts)
+                  NOBR (Pretty.str s) typargs') ts) dicts)
           | SOME (k, Complex_printer print) =>
               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
                 (ts ~~ take k dom))
@@ -148,21 +148,21 @@
             print' fxy ts
           else
             Pretty.block (print' BR ts1 :: map (fn t => Pretty.block
-              [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts2)
+              [Pretty.str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, Pretty.str ")"]) ts2)
         else
           print_term tyvars is_pat some_thm vars fxy (vs_tys `|==> (IConst const `$$ ts1, rty))
       end
     and print_bind tyvars some_thm fxy p =
       gen_print_bind (print_term tyvars true) some_thm fxy p
     and print_case tyvars some_thm vars fxy { clauses = [], ... } =
-          (brackify fxy o Pretty.breaks o map str) ["sys.error(\"empty case\")"]
+          (brackify fxy o Pretty.breaks o map Pretty.str) ["sys.error(\"empty case\")"]
       | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
           let
             val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr);
             fun print_match_val ((pat, ty), t) vars =
               vars
               |> print_bind tyvars some_thm BR pat
-              |>> (fn p => (false, concat [str "val", p, str "=",
+              |>> (fn p => (false, concat [Pretty.str "val", p, Pretty.str "=",
                 constraint (print_term tyvars false some_thm vars NOBR t) (print_typ tyvars BR ty)]));
             fun print_match_seq t vars =
               ((true, print_term tyvars false some_thm vars NOBR t), vars);
@@ -177,30 +177,30 @@
             val all_seps_ps = seps_ps @ [(true, print_term tyvars false some_thm vars' NOBR body)];
             fun insert_seps [(_, p)] = [p]
               | insert_seps ((_, p) :: (seps_ps as (sep, _) :: _)) =
-                  (if sep then Pretty.block [p, str ";"] else p) :: insert_seps seps_ps
-          in brackify_block fxy (str "{") (insert_seps all_seps_ps) (str "}") end
+                  (if sep then Pretty.block [p, Pretty.str ";"] else p) :: insert_seps seps_ps
+          in brackify_block fxy (Pretty.str "{") (insert_seps all_seps_ps) (Pretty.str "}") end
       | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
           let
             fun print_select (pat, body) =
               let
                 val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars;
                 val p_body = print_term tyvars false some_thm vars' NOBR body
-              in concat [str "case", p_pat, str "=>", p_body] end;
+              in concat [Pretty.str "case", p_pat, Pretty.str "=>", p_body] end;
           in
             map print_select clauses
-            |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match {"], str "}")
+            |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, Pretty.str "match {"], Pretty.str "}")
             |> single
-            |> enclose "(" ")"
+            |> Pretty.enclose "(" ")"
           end;
     fun print_context tyvars vs s = applify "[" "]"
-      (fn (v, sort) => (Pretty.block o map str)
+      (fn (v, sort) => (Pretty.block o map Pretty.str)
         (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
-          NOBR (str s) vs;
+          NOBR (Pretty.str s) vs;
     fun print_defhead tyvars vars const vs params tys ty =
-      concat [str "def", constraint (applify "(" ")" (fn (param, ty) =>
-        constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
+      concat [Pretty.str "def", constraint (applify "(" ")" (fn (param, ty) =>
+        constraint ((Pretty.str o lookup_var vars) param) (print_typ tyvars NOBR ty))
           NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
-            str "="];
+            Pretty.str "="];
     fun print_def const (vs, ty) [] =
           let
             val (tys, ty') = Code_Thingol.unfold_fun ty;
@@ -209,7 +209,7 @@
             val vars = intro_vars params reserved;
           in
             concat [print_defhead tyvars vars const vs params tys ty',
-              str ("sys.error(" ^ print_scala_string const ^ ")")]
+              Pretty.str ("sys.error(" ^ print_scala_string const ^ ")")]
           end
       | print_def const (vs, ty) eqs =
           let
@@ -231,7 +231,7 @@
             val vars2 = intro_vars params vars1;
             val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
             fun tuplify [p] = p
-              | tuplify ps = enum "," "(" ")" ps;
+              | tuplify ps = Pretty.enum "," "(" ")" ps;
             fun print_rhs vars' ((_, t), (some_thm, _)) =
               print_term tyvars false some_thm vars' NOBR t;
             fun print_clause (eq as ((ts, _), (some_thm, _))) =
@@ -239,20 +239,20 @@
                 val vars' =
                   intro_vars (build (fold Code_Thingol.add_varnames ts)) vars1;
               in
-                concat [str "case",
+                concat [Pretty.str "case",
                   tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
-                  str "=>", print_rhs vars' eq]
+                  Pretty.str "=>", print_rhs vars' eq]
               end;
             val head = print_defhead tyvars vars2 const vs params tys' ty';
           in if simple then
             concat [head, print_rhs vars2 (hd eqs)]
           else
             Pretty.block_enclose
-              (concat [head, tuplify (map (str o lookup_var vars2) params),
-                str "match {"], str "}")
+              (concat [head, tuplify (map (Pretty.str o lookup_var vars2) params),
+                Pretty.str "match {"], Pretty.str "}")
               (map print_clause eqs)
           end;
-    val print_method = str o Library.enclose "`" "`" o deresolve_full o Constant;
+    val print_method = Pretty.str o enclose "`" "`" o deresolve_full o Constant;
     fun print_inst class (tyco, { vs, inst_params, superinst_params }) =
       let
         val tyvars = intro_tyvars vs reserved;
@@ -264,22 +264,22 @@
             val vars = intro_vars auxs reserved;
             val (aux_dom1, aux_dom2) = chop dom_length aux_dom;
             fun abstract_using [] = []
-              | abstract_using aux_dom = [enum "," "(" ")"
-                  (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
-                  (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
+              | abstract_using aux_dom = [Pretty.enum "," "(" ")"
+                  (map (fn (aux, ty) => constraint ((Pretty.str o lookup_var vars) aux)
+                  (print_typ tyvars NOBR ty)) aux_dom), Pretty.str "=>"];
             val aux_abstr1 = abstract_using aux_dom1;
             val aux_abstr2 = abstract_using aux_dom2;
           in
-            concat ([str "val", print_method classparam, str "="]
+            concat ([Pretty.str "val", print_method classparam, Pretty.str "="]
               @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
                 (const, map (IVar o SOME) auxs))
           end;
       in
-        Pretty.block_enclose (concat [str "implicit def",
+        Pretty.block_enclose (concat [Pretty.str "implicit def",
           constraint (print_context tyvars vs
             ((Library.enclose "`" "`" o deresolve_full o Class_Instance) (tyco, class)))
           (print_dicttyp tyvars classtyp),
-          str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
+          Pretty.str "=", Pretty.str "new", print_dicttyp tyvars classtyp, Pretty.str "{"], Pretty.str "}")
             (map print_classparam_instance (inst_params @ superinst_params))
       end;
     fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) =
@@ -288,29 +288,29 @@
           let
             val tyvars = intro_tyvars (map (rpair []) vs) reserved;
             fun print_co ((co, vs_args), tys) =
-              concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
-                (str ("final case class " ^ deresolve_const co)) vs_args)
-                @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
+              concat [Pretty.block ((applify "[" "]" (Pretty.str o lookup_tyvar tyvars) NOBR
+                (Pretty.str ("final case class " ^ deresolve_const co)) vs_args)
+                @@ Pretty.enum "," "(" ")" (map (fn (v, arg) => constraint (Pretty.str v) (print_typ tyvars NOBR arg))
                   (Name.invent_names (snd reserved) "a" tys))),
-                str "extends",
-                applify "[" "]" (str o lookup_tyvar tyvars) NOBR
-                  ((str o deresolve_tyco) tyco) vs
+                Pretty.str "extends",
+                applify "[" "]" (Pretty.str o lookup_tyvar tyvars) NOBR
+                  ((Pretty.str o deresolve_tyco) tyco) vs
               ];
           in
-            Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
-              NOBR (str ("abstract sealed class " ^ deresolve_tyco tyco)) vs
+            Pretty.chunks (applify "[" "]" (Pretty.str o lookup_tyvar tyvars)
+              NOBR (Pretty.str ("abstract sealed class " ^ deresolve_tyco tyco)) vs
                 :: map print_co cos)
           end
       | print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) =
           let
             val tyvars = intro_tyvars [(v, [class])] reserved;
             fun add_typarg s = Pretty.block
-              [str s, str "[", (str o lookup_tyvar tyvars) v, str "]"];
+              [Pretty.str s, Pretty.str "[", (Pretty.str o lookup_tyvar tyvars) v, Pretty.str "]"];
             fun print_super_classes [] = NONE
-              | print_super_classes classrels = SOME (concat (str "extends"
-                  :: separate (str "with") (map (add_typarg o deresolve_class o snd) classrels)));
+              | print_super_classes classrels = SOME (concat (Pretty.str "extends"
+                  :: separate (Pretty.str "with") (map (add_typarg o deresolve_class o snd) classrels)));
             fun print_classparam_val (classparam, ty) =
-              concat [str "val", constraint (print_method classparam)
+              concat [Pretty.str "val", constraint (print_method classparam)
                 ((print_tupled_typ tyvars o Code_Thingol.unfold_fun) ty)];
             fun print_classparam_def (classparam, ty) =
               let
@@ -320,23 +320,23 @@
                 val auxs = Name.invent (snd proto_vars) "a" (length tys);
                 val vars = intro_vars auxs proto_vars;
               in
-                concat [str "def", constraint (Pretty.block [applify "(" ")"
-                  (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
+                concat [Pretty.str "def", constraint (Pretty.block [applify "(" ")"
+                  (fn (aux, ty) => constraint ((Pretty.str o lookup_var vars) aux)
                   (print_typ tyvars NOBR ty)) NOBR (add_typarg (deresolve_const classparam))
-                  (auxs ~~ tys), str "(implicit ", str implicit_name, str ": ",
-                  add_typarg (deresolve_class class), str ")"]) (print_typ tyvars NOBR ty), str "=",
-                  applify "(" ")" (str o lookup_var vars) NOBR
-                  (Pretty.block [str implicit_name, str ".", print_method classparam]) auxs]
+                  (auxs ~~ tys), Pretty.str "(implicit ", Pretty.str implicit_name, Pretty.str ": ",
+                  add_typarg (deresolve_class class), Pretty.str ")"]) (print_typ tyvars NOBR ty), Pretty.str "=",
+                  applify "(" ")" (Pretty.str o lookup_var vars) NOBR
+                  (Pretty.block [Pretty.str implicit_name, Pretty.str ".", print_method classparam]) auxs]
               end;
           in
             Pretty.chunks (
               (Pretty.block_enclose
-                (concat ([str "trait", (add_typarg o deresolve_class) class]
-                  @ the_list (print_super_classes classrels) @ [str "{"]), str "}")
+                (concat ([Pretty.str "trait", (add_typarg o deresolve_class) class]
+                  @ the_list (print_super_classes classrels) @ [Pretty.str "{"]), Pretty.str "}")
                 (map print_classparam_val classparams))
               :: map print_classparam_def classparams
               @| Pretty.block_enclose
-                (str ("object " ^ deresolve_class class ^ " {"), str "}")
+                (Pretty.str ("object " ^ deresolve_class class ^ " {"), Pretty.str "}")
                 (map (print_inst class) insts)
             )
           end;
@@ -432,8 +432,8 @@
 
     (* print modules *)
     fun print_module _ base _ ps = Pretty.chunks2
-      (str ("object " ^ base ^ " {")
-        :: ps @| str ("} /* object " ^ base ^ " */"));
+      (Pretty.str ("object " ^ base ^ " {")
+        :: ps @| Pretty.str ("} /* object " ^ base ^ " */"));
 
     (* serialization *)
     val p = Pretty.chunks2 (map snd includes
@@ -456,7 +456,7 @@
 in Literals {
   literal_string = print_scala_string,
   literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
-  literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
+  literal_list = fn [] => Pretty.str "Nil" | ps => Pretty.block [Pretty.str "List", Pretty.enum "," "(" ")" ps],
   infix_cons = (6, "::")
 } end;
 
@@ -475,7 +475,7 @@
     [(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
       brackify_infix (1, R) fxy (
         print_typ BR ty1 (*product type vs. tupled arguments!*),
-        str "=>",
+        Pretty.str "=>",
         print_typ (INFX (1, R)) ty2
       )))]))
   #> fold (Code_Target.add_reserved target) [
diff -r 3f875966c3e1 -r ceb4f33d3073 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Mar 30 13:50:06 2025 +0200
+++ b/src/Tools/Code/code_target.ML	Sun Mar 30 13:50:06 2025 +0200
@@ -656,7 +656,7 @@
 
 local
 
-val format_source = Pretty.block0 o Pretty.fbreaks o map Code_Printer.str o split_lines;
+val format_source = Pretty.block0 o Pretty.fbreaks o map Pretty.str o split_lines;
 
 fun eval_source (Literal s) = s
   | eval_source (File p) = File.read p;