# HG changeset patch
# User wenzelm
# Date 1724437264 -7200
# Node ID 232a839ef8e6536d71a402251ff5b11481808acf
# Parent  43c4817375bf0d4346d9d119ec9d5e47ffd6f976
clarified signature: more operations;

diff -r 43c4817375bf -r 232a839ef8e6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Aug 23 18:38:44 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Aug 23 20:21:04 2024 +0200
@@ -155,6 +155,7 @@
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
   val check_case: Proof.context -> bool ->
     string * Position.T -> binding option list -> Rule_Cases.T
+  val is_syntax_const: Proof.context -> string -> bool
   val check_syntax_const: Proof.context -> string * Position.T -> string
   val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
     Proof.context -> Proof.context
@@ -1125,8 +1126,10 @@
 
 (* syntax *)
 
+val is_syntax_const = Syntax.is_const o syntax_of;
+
 fun check_syntax_const ctxt (c, pos) =
-  if Syntax.is_const (syntax_of ctxt) c then c
+  if is_syntax_const ctxt c then c
   else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
 
 fun syntax add mode args ctxt =
diff -r 43c4817375bf -r 232a839ef8e6 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 18:38:44 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 20:21:04 2024 +0200
@@ -620,7 +620,7 @@
           in (t1' $ t2', seen'') end;
   in #1 (prune (tm, [])) end;
 
-fun mark_atoms is_syntax_const ctxt tm =
+fun mark_atoms ctxt tm =
   let
     val {structs, fixes} = Syntax_Trans.get_idents ctxt;
     val show_structs = Config.get ctxt show_structs;
@@ -631,7 +631,7 @@
       | mark (t $ u) = mark t $ mark u
       | mark (Abs (x, T, t)) = Abs (x, T, mark t)
       | mark (t as Const (c, T)) =
-          if is_syntax_const c then t
+          if Proof_Context.is_syntax_const ctxt c then t
           else Const (Lexicon.mark_const c, T)
       | mark (t as Free (x, T)) =
           let val i = find_index (fn s => s = x) structs + 1 in
@@ -651,8 +651,6 @@
 
 fun term_to_ast ctxt trf tm =
   let
-    val is_syntax_const = Syntax.is_const (Proof_Context.syntax_of ctxt);
-
     val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
     val show_markup = Config.get ctxt show_markup;
 
@@ -694,7 +692,7 @@
     |> mark_aprop
     |> show_types ? prune_types
     |> Variable.revert_bounds ctxt
-    |> mark_atoms is_syntax_const ctxt
+    |> mark_atoms ctxt
     |> ast_of
   end;