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