# HG changeset patch
# User wenzelm
# Date 1632163418 -7200
# Node ID b9a3d2fb53e019dc2bbfc31b6ab2aaed9e199a88
# Parent  d882abae33790ec0ff229fc99422349f60af6519
clarified signature;

diff -r d882abae3379 -r b9a3d2fb53e0 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Sep 20 20:22:32 2021 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 20 20:43:38 2021 +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 check_syntax_const: Proof.context -> string * Position.T -> string
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
   val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
@@ -1123,6 +1124,13 @@
 end;
 
 
+(* syntax *)
+
+fun check_syntax_const ctxt (c, pos) =
+  if is_some (Syntax.lookup_const (syn_of ctxt) c) then c
+  else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
+
+
 (* notation *)
 
 local
diff -r d882abae3379 -r b9a3d2fb53e0 src/Pure/ML/ml_antiquotations1.ML
--- a/src/Pure/ML/ml_antiquotations1.ML	Mon Sep 20 20:22:32 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations1.ML	Mon Sep 20 20:43:38 2021 +0200
@@ -171,10 +171,8 @@
     (const_name (fn (_, c) => Lexicon.mark_const c)) #>
 
   ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close>
-    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (c, pos)) =>
-      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
-      then ML_Syntax.print_string c
-      else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
+    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
+      ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #>
 
   ML_Antiquotation.inline_embedded \<^binding>\<open>const\<close>
     (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional