--- 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 *)