--- a/src/Pure/Isar/proof_context.ML Sat Dec 14 22:26:27 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML Sat Dec 14 23:48:45 2024 +0100
@@ -167,6 +167,7 @@
Proof.context -> Proof.context
val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
Context.generic -> Context.generic
+ val generic_syntax_deps: (string * string list) list -> Context.generic -> Context.generic
val translations: bool -> Ast.ast Syntax.trrule list -> Proof.context -> Proof.context
val generic_translations: bool -> Ast.ast Syntax.trrule list -> Context.generic -> Context.generic
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
@@ -1219,6 +1220,10 @@
fun generic_syntax add mode args =
Context.mapping (Sign.syntax_global add mode args) (syntax add mode args);
+fun generic_syntax_deps args =
+ Context.mapping (Sign.syntax_deps args)
+ (fn ctxt => map_syntax (Local_Syntax.syntax_deps ctxt args) ctxt);
+
(* translations *)