# HG changeset patch
# User wenzelm
# Date 1728736179 -7200
# Node ID ee8c3375cd397be5aa9a024ce24769ef7e2f5bbe
# Parent  ece9fe9bf440132767626c93e31041bca6aabb22
clarified signature;

diff -r ece9fe9bf440 -r ee8c3375cd39 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Sat Oct 12 14:22:19 2024 +0200
+++ b/src/Pure/Syntax/ast.ML	Sat Oct 12 14:29:39 2024 +0200
@@ -15,6 +15,7 @@
   val ast_ord: ast ord
   structure Table: TABLE
   structure Set: SET
+  val pretty_var: string -> Pretty.T
   val pretty_ast: ast -> Pretty.T
   val pretty_rule: ast * ast -> Pretty.T
   val strip_positions: ast -> ast
@@ -81,11 +82,13 @@
 
 (* print asts in a LISP-like style *)
 
+fun pretty_var x =
+  (case Term_Position.decode x of
+    SOME pos => Term_Position.pretty pos
+  | NONE => Pretty.str x);
+
 fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
-  | pretty_ast (Variable x) =
-      (case Term_Position.decode x of
-        SOME pos => Term_Position.pretty pos
-      | NONE => Pretty.str x)
+  | pretty_ast (Variable x) = pretty_var x
   | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
 
 fun pretty_rule (lhs, rhs) =
diff -r ece9fe9bf440 -r ee8c3375cd39 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sat Oct 12 14:22:19 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat Oct 12 14:29:39 2024 +0200
@@ -289,8 +289,8 @@
         | NONE => astT (trf a ctxt args, p) handle Match => prnt ([], tabs))
       end
 
-    and astT (c as Ast.Constant a, p) = combT (c, a, [], p)
-      | astT (ast as Ast.Variable _, _) = [Ast.pretty_ast ast]
+    and astT (Ast.Variable x, _) = [Ast.pretty_var x]
+      | astT (c as Ast.Constant a, p) = combT (c, a, [], p)
       | astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p)
       | astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
       | astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);