# HG changeset patch
# User wenzelm
# Date 1729350014 -7200
# Node ID 0123c6c8f38ab972831c477416843b1a1caf902f
# Parent  785c0241d7b8f0734961862e1d8d573d8b628a94
clarified signature;

diff -r 785c0241d7b8 -r 0123c6c8f38a src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sat Oct 19 16:54:34 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Sat Oct 19 17:00:14 2024 +0200
@@ -37,6 +37,7 @@
   type pretty_ops =
    {trf: string -> Proof.context -> Ast.ast list -> Ast.ast,
     constrain_block: Ast.ast -> Markup.output Pretty.block,
+    constrain_trans: Ast.ast -> Ast.ast -> Pretty.T option,
     markup_trans: string -> Ast.ast list -> Pretty.T option,
     markup: string -> Markup.T list,
     extern: string -> xstring}
@@ -228,6 +229,7 @@
 type pretty_ops =
  {trf: string -> Proof.context -> Ast.ast list -> Ast.ast,
   constrain_block: Ast.ast -> Markup.output Pretty.block,
+  constrain_trans: Ast.ast -> Ast.ast -> Pretty.T option,
   markup_trans: string -> Ast.ast list -> Pretty.T option,
   markup: string -> Markup.T list,
   extern: string -> xstring};
@@ -241,8 +243,8 @@
       else if curried then Syntax_Trans.applC_ast_tr'
       else Syntax_Trans.appl_ast_tr';
 
-    fun constrain_trans (Ast.Appl [Ast.Constant (a as "_constrain"), ast, ty]) =
-          #markup_trans ops a [ast, ty]
+    fun constrain_trans (Ast.Appl [Ast.Constant "_constrain", ast, ty]) =
+          #constrain_trans ops ast ty
       | constrain_trans _ = NONE;
 
     fun main _ (Ast.Variable x) = [Ast.pretty_var x]
diff -r 785c0241d7b8 -r 0123c6c8f38a src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Oct 19 16:54:34 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Oct 19 17:00:14 2024 +0200
@@ -808,8 +808,8 @@
 
     and pretty_ast flags m =
       Printer.pretty flags ctxt prtabs
-        {trf = trf, constrain_block = constrain_block true, markup_trans = markup_trans,
-          markup = markup, extern = extern}
+        {trf = trf, constrain_block = constrain_block true, constrain_trans = constrain_trans,
+          markup_trans = markup_trans, markup = markup, extern = extern}
       #> Pretty.markup m
 
     and markup_ast is_typing a A =