# HG changeset patch
# User wenzelm
# Date 1727340696 -7200
# Node ID 4547a3674d10ddc84bf00de1f02f59018596be4e
# Parent  5e4ff05499604aff000b934ba4da67c10f0e0748
tuned;

diff -r 5e4ff0549960 -r 4547a3674d10 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Thu Sep 26 00:06:00 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Thu Sep 26 10:51:36 2024 +0200
@@ -131,17 +131,13 @@
 
 (* xprod_to_fmt *)
 
-local
+fun make_string s = String ([], s);
+fun make_literal s = String (Lexicon.literal_markup s, s);
 
 fun make_arg (s, p) =
   (if s = "type" then TypArg else Arg)
   (if Lexicon.is_terminal s then 1000 else p);
 
-in
-
-fun make_string s = String ([], s);
-fun make_literal s = String (Lexicon.literal_markup s, s);
-
 fun xprod_to_fmt (Syntax_Ext.XProd (_, _, "", _)) = NONE
   | xprod_to_fmt (Syntax_Ext.XProd (_, xsymbs, const, pri)) =
       let
@@ -169,8 +165,6 @@
         | _ => raise Fail "Unbalanced pretty-printing blocks")
       end;
 
-end;
-
 
 (* empty, extend, merge prtabs *)