more explicit context for syn_ext/mixfix operations, but it often degenerates to background theory;

--- a/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -47,10 +47,11 @@
 *)
 fun transform thy (c, T, mx) =
   let
+    val thy_ctxt = Proof_Context.init_global thy
     fun syntax b = Lexicon.mark_const (Sign.full_bname thy b)
     val c1 = Binding.name_of c
     val c2 = c1 ^ "_cont_syntax"
-    val n = Mixfix.mixfix_args mx
+    val n = Mixfix.mixfix_args thy_ctxt mx
   in
     ((c, T, NoSyn),
       (Binding.name c2, change_arrow n T, mx),
@@ -60,11 +61,12 @@
 fun cfun_arity (Type (n, [_, T])) = if n = \<^type_name>\<open>cfun\<close> then 1 + cfun_arity T else 0
   | cfun_arity _ = 0
 
-fun is_contconst (_, _, NoSyn) = false
-  | is_contconst (_, _, Binder _) = false    (* FIXME ? *)
-  | is_contconst (c, T, mx) =
+fun is_contconst _ (_, _, NoSyn) = false
+  | is_contconst _ (_, _, Binder _) = false    (* FIXME ? *)
+  | is_contconst thy (c, T, mx) =
       let
-        val n = Mixfix.mixfix_args mx handle ERROR msg =>
+        val thy_ctxt = Proof_Context.init_global thy
+        val n = Mixfix.mixfix_args thy_ctxt mx handle ERROR msg =>
           cat_error msg ("in mixfix annotation for " ^ Binding.print c)
       in cfun_arity T >= n end
 
@@ -76,7 +78,7 @@
 fun gen_add_consts prep_typ raw_decls thy =
   let
     val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls
-    val (contconst_decls, normal_decls) = List.partition is_contconst decls
+    val (contconst_decls, normal_decls) = List.partition (is_contconst thy) decls
     val transformed_decls = map (transform thy) contconst_decls
   in
     thy

--- a/src/Pure/Isar/class.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/Isar/class.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -438,7 +438,7 @@
     thy
     |> Sign.add_abbrev (#1 prmode) (b, Logic.varify_types_global rhs')
     |> snd
-    |> with_syntax ? Sign.notation true prmode [(Const (c, fastype_of rhs), mx)]
+    |> with_syntax ? Sign.notation_global true prmode [(Const (c, fastype_of rhs), mx)]
     |> with_syntax ? register_operation class (c, rhs)
         (#1 prmode = Print_Mode.input)
     |> Sign.add_const_constraint (c, SOME (fastype_of rhs'))

--- a/src/Pure/Isar/generic_target.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -412,7 +412,7 @@
   Local_Theory.background_theory_result
     (Sign.add_abbrev (#1 prmode) (b, global_rhs) #->
       (fn (lhs, _) =>  (* FIXME type_params!? *)
-        Sign.notation true prmode
+        Sign.notation_global true prmode
           [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs))
   #-> (fn lhs =>
         standard_const (op <>) prmode

--- a/src/Pure/Isar/proof.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -604,7 +604,7 @@
       let
         val ctxt' =
           ctxt |> is_none (Variable.default_type ctxt x) ?
-            Variable.declare_constraints (Free (x, Mixfix.default_constraint mx));
+            Variable.declare_constraints (Free (x, Mixfix.default_constraint ctxt mx));
         val t = Free (#1 (Proof_Context.inferred_param x ctxt'));
       in ((t, mx), ctxt') end
   | t => ((t, mx), ctxt));

--- a/src/Pure/Isar/proof_context.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -377,18 +377,25 @@
 
 (* theory transfer *)
 
-fun transfer_syntax thy ctxt = ctxt |>
-  map_syntax (Local_Syntax.rebuild thy) |>
-  map_tsig (fn tsig as (local_tsig, global_tsig) =>
-    let val thy_tsig = Sign.tsig_of thy in
-      if Type.eq_tsig (thy_tsig, global_tsig) then tsig
-      else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
-    end) |>
-  map_consts (fn consts as (local_consts, global_consts) =>
-    let val thy_consts = Sign.consts_of thy in
-      if Consts.eq_consts (thy_consts, global_consts) then consts
-      else (Consts.merge (local_consts, thy_consts), thy_consts)  (*historic merge order*)
-    end);
+fun transfer_syntax thy ctxt =
+  let
+    val thy_ctxt =
+      Proof_Context.init_global thy
+      |> Context_Position.restore_visible ctxt;
+  in
+    ctxt |>
+    map_syntax (Local_Syntax.rebuild thy_ctxt) |>
+    map_tsig (fn tsig as (local_tsig, global_tsig) =>
+      let val thy_tsig = Sign.tsig_of thy in
+        if Type.eq_tsig (thy_tsig, global_tsig) then tsig
+        else (Type.merge_tsig (Context.Proof ctxt) (local_tsig, thy_tsig), thy_tsig)  (*historic merge order*)
+      end) |>
+    map_consts (fn consts as (local_consts, global_consts) =>
+      let val thy_consts = Sign.consts_of thy in
+        if Consts.eq_consts (thy_consts, global_consts) then consts
+        else (Consts.merge (local_consts, thy_consts), thy_consts)  (*historic merge order*)
+      end)
+  end;
 
 fun transfer thy = Context.raw_transfer thy #> transfer_syntax thy;
 
@@ -1081,7 +1088,7 @@
 (* variables *)
 
 fun declare_var (x, opt_T, mx) ctxt =
-  let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint mx)
+  let val T = (case opt_T of SOME T => T | NONE => Mixfix.default_constraint ctxt mx)
   in (T, ctxt |> Variable.declare_constraints (Free (x, T))) end;
 
 fun add_syntax vars ctxt =
@@ -1137,7 +1144,7 @@
   in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end;
 
 fun generic_syntax add mode args =
-  Context.mapping (Sign.syntax add mode args) (syntax add mode args);
+  Context.mapping (Sign.syntax_global add mode args) (syntax add mode args);
 
 
 (* notation *)
@@ -1171,14 +1178,14 @@
         val T' = Morphism.typ phi T;
         val similar = (case (T, T') of (Type (c, _), Type (c', _)) => c = c' | _ => false);
       in if similar then SOME (T', mx) else NONE end);
-  in Context.mapping (Sign.type_notation add mode args') (type_notation add mode args') end;
+  in Context.mapping (Sign.type_notation_global add mode args') (type_notation add mode args') end;
 
 fun generic_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (t, mx) =>
       let val t' = Morphism.term phi t
       in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
-  in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
+  in Context.mapping (Sign.notation_global add mode args') (notation add mode args') end;
 
 end;
 

--- a/src/Pure/Proof/proof_syntax.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -46,7 +46,7 @@
   |> Sign.add_nonterminals_global
     [Binding.make ("param", \<^here>),
      Binding.make ("params", \<^here>)]
-  |> Sign.syntax true Syntax.mode_default
+  |> Sign.syntax_global true Syntax.mode_default
     [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
      ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
      ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),

--- a/src/Pure/Syntax/local_syntax.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -10,7 +10,7 @@
   type T
   val syntax_of: T -> Syntax.syntax
   val init: theory -> T
-  val rebuild: theory -> T -> T
+  val rebuild: Proof.context -> T -> T
   datatype kind = Type | Const | Fixed
   val add_syntax: Proof.context -> (kind * (string * typ * mixfix)) list ->
     T -> {structs: string list, fixes: string list} option * T
@@ -42,20 +42,21 @@
 fun map_syntax f (Syntax {thy_syntax, local_syntax, mode, mixfixes}) =
   make_syntax (f (thy_syntax, local_syntax, mode, mixfixes));
 
-fun is_consistent thy (Syntax {thy_syntax, ...}) =
-  Syntax.eq_syntax (Sign.syntax_of thy, thy_syntax);
+fun is_consistent ctxt (Syntax {thy_syntax, ...}) =
+  Syntax.eq_syntax (Sign.syntax_of (Proof_Context.theory_of ctxt), thy_syntax);
 
 fun syntax_of (Syntax {local_syntax, ...}) = local_syntax;
 
 
 (* build syntax *)
 
-fun build_syntax thy mode mixfixes =
+fun build_syntax ctxt mode mixfixes =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val thy_syntax = Sign.syntax_of thy;
-    fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
+    fun update_gram ((true, add, m), decls) = Syntax.update_type_gram ctxt add m decls
       | update_gram ((false, add, m), decls) =
-          Syntax.update_const_gram add (Sign.logical_types thy) m decls;
+          Syntax.update_const_gram ctxt add (Sign.logical_types thy) m decls;
 
     val local_syntax = thy_syntax
       |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
@@ -65,9 +66,9 @@
   let val thy_syntax = Sign.syntax_of thy
   in make_syntax (thy_syntax, thy_syntax, Syntax.mode_default, []) end;
 
-fun rebuild thy (syntax as Syntax {mode, mixfixes, ...}) =
-  if is_consistent thy syntax then syntax
-  else build_syntax thy mode mixfixes;
+fun rebuild ctxt (syntax as Syntax {mode, mixfixes, ...}) =
+  if is_consistent ctxt syntax then syntax
+  else build_syntax ctxt mode mixfixes;
 
 
 (* mixfix declarations *)
@@ -104,7 +105,7 @@
             else subtract (op =) new_structs (#structs idents),
            fixes = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' []};
 
-        val syntax' = build_syntax (Proof_Context.theory_of ctxt) mode mixfixes';
+        val syntax' = build_syntax ctxt mode mixfixes';
       in (if idents = idents' then NONE else SOME idents', syntax') end);
 
 fun add_syntax ctxt = update_syntax ctxt true;

--- a/src/Pure/Syntax/mixfix.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -26,12 +26,13 @@
   val pos_of: mixfix -> Position.T
   val reset_pos: mixfix -> mixfix
   val pretty_mixfix: mixfix -> Pretty.T
-  val mixfix_args: mixfix -> int
-  val default_constraint: mixfix -> typ
+  val mixfix_args: Proof.context -> mixfix -> int
+  val default_constraint: Proof.context -> mixfix -> typ
   val make_type: int -> typ
   val binder_name: string -> string
-  val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
-  val syn_ext_consts: string list -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
+  val syn_ext_types: Proof.context -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
+  val syn_ext_consts: Proof.context -> string list -> (string * typ * mixfix) list ->
+    Syntax_Ext.syn_ext
 end;
 
 structure Mixfix: MIXFIX =
@@ -117,19 +118,20 @@
 
 (* syntax specifications *)
 
-fun mixfix_args NoSyn = 0
-  | mixfix_args (Mixfix (sy, _, _, _)) = Syntax_Ext.mixfix_args sy
-  | mixfix_args (Infix (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
-  | mixfix_args (Infixl (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
-  | mixfix_args (Infixr (sy, _, _)) = 2 + Syntax_Ext.mixfix_args sy
-  | mixfix_args (Binder _) = 1
-  | mixfix_args (Structure _) = 0;
+fun mixfix_args ctxt =
+  fn NoSyn => 0
+   | Mixfix (sy, _, _, _) => Syntax_Ext.mixfix_args ctxt sy
+   | Infix (sy, _, _) => 2 + Syntax_Ext.mixfix_args ctxt sy
+   | Infixl (sy, _, _) => 2 + Syntax_Ext.mixfix_args ctxt sy
+   | Infixr (sy, _, _) => 2 + Syntax_Ext.mixfix_args ctxt sy
+   | Binder _ => 1
+   | Structure _ => 0;
 
 
 (* default type constraint *)
 
-fun default_constraint (Binder _) = (dummyT --> dummyT) --> dummyT
-  | default_constraint mx = replicate (mixfix_args mx) dummyT ---> dummyT;
+fun default_constraint _ (Binder _) = (dummyT --> dummyT) --> dummyT
+  | default_constraint ctxt mx = replicate (mixfix_args ctxt mx) dummyT ---> dummyT;
 
 
 (* mixfix template *)
@@ -154,7 +156,7 @@
 val typeT = Type ("type", []);
 fun make_type n = replicate n typeT ---> typeT;
 
-fun syn_ext_types type_decls =
+fun syn_ext_types ctxt type_decls =
   let
     fun mk_infix sy ty t p1 p2 p3 pos =
       Syntax_Ext.Mfix
@@ -172,7 +174,7 @@
       | (t, _, _) => error ("Bad mixfix declaration for " ^ quote t ^ Position.here (pos_of mx)));
 
     fun check_args (_, ty, mx) (SOME (Syntax_Ext.Mfix (sy, _, _, _, _, _))) =
-          if length (Term.binder_types ty) = Syntax_Ext.mfix_args sy then ()
+          if length (Term.binder_types ty) = Syntax_Ext.mfix_args ctxt sy then ()
           else
             error ("Bad number of type constructor arguments in mixfix annotation" ^
               Position.here (pos_of mx))
@@ -183,7 +185,7 @@
     val mfix = map mfix_of type_decls;
     val _ = map2 check_args type_decls mfix;
     val consts = map (fn (t, _, _) => (t, [])) type_decls;
-  in Syntax_Ext.syn_ext [] (map_filter I mfix) consts ([], [], [], []) ([], []) end;
+  in Syntax_Ext.syn_ext ctxt [] (map_filter I mfix) consts ([], [], [], []) ([], []) end;
 
 
 (* syn_ext_consts *)
@@ -195,7 +197,7 @@
   let val sy' = Input.source_explode (Input.reset_pos sy); 
   in Symbol_Pos.explode0 "'(" @ sy' @ Symbol_Pos.explode0 "')" end
 
-fun syn_ext_consts logical_types const_decls =
+fun syn_ext_consts ctxt logical_types const_decls =
   let
     fun mk_infix sy ty c p1 p2 p3 pos =
       [Syntax_Ext.Mfix (mk_prefix sy, ty, c, [], 1000, Position.none),
@@ -238,7 +240,9 @@
     val consts =
       map (fn (c, b) => (c, [b])) binders @
       map (fn (c, _, _) => (c, [])) const_decls;
-  in Syntax_Ext.syn_ext logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) end;
+  in
+    Syntax_Ext.syn_ext ctxt logical_types mfix consts ([], binder_trs, binder_trs', []) ([], [])
+  end;
 
 end;
 

--- a/src/Pure/Syntax/syntax.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -104,17 +104,18 @@
     Print_Rule of 'a * 'a |
     Parse_Print_Rule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
-  val update_trfuns:
+  val update_trfuns: Proof.context ->
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
-  val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
-  val update_const_gram: bool -> string list ->
+  val update_type_gram: Proof.context -> bool -> mode -> (string * typ * mixfix) list ->
+    syntax -> syntax
+  val update_const_gram: Proof.context -> bool -> string list ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
-  val update_consts: (string * string list) list -> syntax -> syntax
-  val update_trrules: Ast.ast trrule list -> syntax -> syntax
-  val remove_trrules: Ast.ast trrule list -> syntax -> syntax
+  val update_consts: Proof.context -> (string * string list) list -> syntax -> syntax
+  val update_trrules: Proof.context -> Ast.ast trrule list -> syntax -> syntax
+  val remove_trrules: Proof.context -> Ast.ast trrule list -> syntax -> syntax
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
@@ -707,18 +708,19 @@
 
 (** modify syntax **)
 
-val update_trfuns = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns;
+fun update_trfuns ctxt = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns ctxt;
 
-fun update_type_gram add prmode decls =
-  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
+fun update_type_gram ctxt add prmode decls =
+  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types ctxt decls);
 
-fun update_const_gram add logical_types prmode decls =
-  (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts logical_types decls);
+fun update_const_gram ctxt add logical_types prmode decls =
+  (if add then update_syntax else remove_syntax) prmode
+    (Mixfix.syn_ext_consts ctxt logical_types decls);
 
-val update_consts = update_syntax mode_default o Syntax_Ext.syn_ext_consts;
+val update_consts = update_syntax mode_default oo Syntax_Ext.syn_ext_consts;
 
-val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
-val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
+fun update_trrules ctxt = update_syntax mode_default o Syntax_Ext.syn_ext_rules ctxt o check_rules;
+fun remove_trrules ctxt = remove_syntax mode_default o Syntax_Ext.syn_ext_rules ctxt o check_rules;
 
 
 open Lexicon.Syntax;

--- a/src/Pure/Syntax/syntax_ext.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -29,18 +29,18 @@
       print_translation: (string * ((Proof.context -> typ -> term list -> term) * stamp)) list,
       print_rules: (Ast.ast * Ast.ast) list,
       print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list}
-  val mfix_args: Symbol_Pos.T list -> int
-  val mixfix_args: Input.source -> int
+  val mfix_args: Proof.context -> Symbol_Pos.T list -> int
+  val mixfix_args: Proof.context -> Input.source -> int
   val escape: string -> string
-  val syn_ext: string list -> mfix list ->
+  val syn_ext: Proof.context -> string list -> mfix list ->
     (string * string list) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
     (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
-  val syn_ext_consts: (string * string list) list -> syn_ext
-  val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
-  val syn_ext_trfuns:
+  val syn_ext_consts: Proof.context -> (string * string list) list -> syn_ext
+  val syn_ext_rules: Proof.context -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
+  val syn_ext_trfuns: Proof.context ->
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
@@ -263,18 +263,21 @@
 
 in
 
-fun read_mfix ss =
+fun read_mfix ctxt ss =
   let
     val xsymbs =
       (case Scan.error (Scan.finite Symbol_Pos.stopper scan_symbs) ss of
         (res, []) => map_filter I res
       | (_, (_, pos) :: _) => error (err_prefix ^ "bad input" ^ Position.here pos));
-    val _ = Position.reports (maps reports_of xsymbs);
-    val _ = Position.reports_text (maps reports_text_of xsymbs);
+    val _ = Context_Position.reports ctxt (maps reports_of xsymbs);
+    val _ = Context_Position.reports_text ctxt (maps reports_text_of xsymbs);
   in xsymbs end;
 
-val mfix_args = length o filter (is_argument o #1) o read_mfix o map (apsnd (K Position.none));
-val mixfix_args = mfix_args o Input.source_explode;
+fun mfix_args ctxt =
+  let val ctxt' = Context_Position.set_visible false ctxt
+  in length o filter (is_argument o #1) o read_mfix ctxt' o map (apsnd (K Position.none)) end;
+
+fun mixfix_args ctxt = mfix_args ctxt o Input.source_explode;
 
 val escape = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
 
@@ -283,13 +286,13 @@
 
 (* mfix_to_xprod *)
 
-fun mfix_to_xprod logical_types (Mfix (sy, typ, const, pris, pri, pos)) =
+fun mfix_to_xprod ctxt logical_types (Mfix (sy, typ, const, pris, pri, pos)) =
   let
     val nonterm_for_lhs = the_default "logic" o try dest_Type_name;
     val nonterm_for_rhs = the_default "any" o try dest_Type_name;
 
     val _ = Position.report pos Markup.language_mixfix;
-    val symbs0 = read_mfix sy;
+    val symbs0 = read_mfix ctxt sy;
 
     fun err_in_mixfix msg = error (msg ^ " in mixfix annotation" ^ Position.here pos);
 
@@ -396,12 +399,12 @@
 
 (* syn_ext *)
 
-fun syn_ext logical_types mfixes consts trfuns (parse_rules, print_rules) =
+fun syn_ext ctxt logical_types mfixes consts trfuns (parse_rules, print_rules) =
   let
     val (parse_ast_translation, parse_translation, print_translation,
       print_ast_translation) = trfuns;
 
-    val xprod_results = map (mfix_to_xprod logical_types) mfixes;
+    val xprod_results = map (mfix_to_xprod ctxt logical_types) mfixes;
     val xprods = map #1 xprod_results;
     val consts' = map_filter #2 xprod_results;
     val parse_rules' = rev (map_filter #3 xprod_results);
@@ -419,9 +422,9 @@
   end;
 
 
-fun syn_ext_consts consts = syn_ext [] [] consts ([], [], [], []) ([], []);
-fun syn_ext_rules rules = syn_ext [] [] [] ([], [], [], []) rules;
-fun syn_ext_trfuns trfuns = syn_ext [] [] [] trfuns ([], []);
+fun syn_ext_consts ctxt consts = syn_ext ctxt [] [] consts ([], [], [], []) ([], []);
+fun syn_ext_rules ctxt rules = syn_ext ctxt [] [] [] ([], [], [], []) rules;
+fun syn_ext_trfuns ctxt trfuns = syn_ext ctxt [] [] [] trfuns ([], []);
 
 fun stamp_trfun s (c, f) = (c, (f, s));
 fun mk_trfun tr = stamp_trfun (stamp ()) tr;

--- a/src/Pure/pure_thy.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/pure_thy.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -55,8 +55,8 @@
 
 val old_appl_syntax_setup =
   Old_Appl_Syntax.put true #>
-  Sign.syntax false Syntax.mode_default applC_syntax #>
-  Sign.syntax true Syntax.mode_default appl_syntax;
+  Sign.syntax_global false Syntax.mode_default applC_syntax #>
+  Sign.syntax_global true Syntax.mode_default appl_syntax;
 
 
 (* main content *)
@@ -87,8 +87,8 @@
         "tvar_position", "id_position", "longid_position", "var_position",
         "str_position", "string_position", "cartouche_position", "type_name",
         "class_name"]))
-  #> Sign.syntax true Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
-  #> Sign.syntax true Syntax.mode_default
+  #> Sign.syntax_global true Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
+  #> Sign.syntax_global true Syntax.mode_default
    [("",            typ "prop' \<Rightarrow> prop",               Mixfix.mixfix "_"),
     ("",            typ "logic \<Rightarrow> any",                Mixfix.mixfix "_"),
     ("",            typ "prop' \<Rightarrow> any",                Mixfix.mixfix "_"),
@@ -184,8 +184,8 @@
     ("_sort_constraint", typ "type \<Rightarrow> prop",           Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
     (const "Pure.term", typ "logic \<Rightarrow> prop",           Mixfix.mixfix "TERM _"),
     (const "Pure.conjunction", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("&&&", 2))]
-  #> Sign.syntax true Syntax.mode_default applC_syntax
-  #> Sign.syntax true (Print_Mode.ASCII, true)
+  #> Sign.syntax_global true Syntax.mode_default applC_syntax
+  #> Sign.syntax_global true (Print_Mode.ASCII, true)
    [(tycon "fun",         typ "type \<Rightarrow> type \<Rightarrow> type",   mixfix ("(_/ => _)", [1, 0], 0)),
     ("_bracket",          typ "types \<Rightarrow> type \<Rightarrow> type",  mixfix ("([_]/ => _)", [0, 0], 0)),
     ("_lambda",           typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic",  mixfix ("(3%_./ _)", [0, 3], 3)),
@@ -195,7 +195,7 @@
     ("_DDDOT",            typ "aprop",                  Mixfix.mixfix "..."),
     ("_bigimpl",          typ "asms \<Rightarrow> prop \<Rightarrow> prop",   mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
     ("_DDDOT",            typ "logic",                  Mixfix.mixfix "...")]
-  #> Sign.syntax true ("", false)
+  #> Sign.syntax_global true ("", false)
    [(const "Pure.prop", typ "prop \<Rightarrow> prop", mixfix ("_", [0], 0))]
   #> Sign.add_consts
    [(qualify (Binding.make ("eq", \<^here>)), typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("\<equiv>", 2)),

--- a/src/Pure/sign.ML	Tue Sep 17 17:05:37 2024 +0200
+++ b/src/Pure/sign.ML	Tue Sep 17 17:51:55 2024 +0200
@@ -76,10 +76,12 @@
   val add_nonterminals: Proof.context -> binding list -> theory -> theory
   val add_nonterminals_global: binding list -> theory -> theory
   val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
-  val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
+  val syntax: Proof.context -> bool -> Syntax.mode -> (string * typ * mixfix) list ->
+    theory -> theory
+  val syntax_global: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   val syntax_deps: (string * string list) list -> theory -> theory
-  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
-  val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
+  val type_notation_global: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
+  val notation_global: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
   val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory
   val add_consts: (binding * typ * mixfix) list -> theory -> theory
@@ -157,6 +159,8 @@
 fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts));
 fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
 
+fun update_syn_global f args thy = map_syn (f (Proof_Context.init_global thy) args) thy;
+
 
 (* linear change discipline *)
 
@@ -357,7 +361,7 @@
 fun add_type ctxt (b, n, mx) thy = thy |> map_sign (fn (syn, tsig, consts) =>
   let
     val type_syntax = (Lexicon.mark_type (full_name thy b), Mixfix.make_type n, mx);
-    val syn' = Syntax.update_type_gram true Syntax.mode_default [type_syntax] syn;
+    val syn' = Syntax.update_type_gram ctxt true Syntax.mode_default [type_syntax] syn;
     val tsig' = Type.add_type (inherit_naming thy ctxt) (b, n) tsig;
   in (syn', tsig', consts) end);
 
@@ -382,29 +386,34 @@
 
 (* modify syntax *)
 
-fun syntax add mode args thy =
+fun syntax ctxt add mode args thy =
   let
     fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy T, mx)
       handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
-  in thy |> map_syn (Syntax.update_const_gram add (logical_types thy) mode (map prep args)) end;
+  in thy |> map_syn (Syntax.update_const_gram ctxt add (logical_types thy) mode (map prep args)) end;
+
+fun syntax_global add mode args thy =
+  syntax (Proof_Context.init_global thy) add mode args thy;
 
-val syntax_deps = map_syn o Syntax.update_consts;
+val syntax_deps = update_syn_global Syntax.update_consts;
 
-fun type_notation add mode args =
+fun type_notation_global add mode args thy =
   let
+    val thy_ctxt = Proof_Context.init_global thy;
     fun type_syntax (Type (c, args), mx) =
           SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx)
       | type_syntax _ = NONE;
-  in map_syn (Syntax.update_type_gram add mode (map_filter type_syntax args)) end;
+  in map_syn (Syntax.update_type_gram thy_ctxt add mode (map_filter type_syntax args)) thy end;
 
-fun notation add mode args thy =
+fun notation_global add mode args thy =
   let
+    val thy_ctxt = Proof_Context.init_global thy;
     fun const_syntax (Const (c, _), mx) =
           (case try (Consts.type_scheme (consts_of thy)) c of
             SOME T => SOME (Lexicon.mark_const c, T, mx)
           | NONE => NONE)
       | const_syntax _ = NONE;
-  in syntax add mode (map_filter const_syntax args) thy end;
+  in syntax thy_ctxt add mode (map_filter const_syntax args) thy end;
 
 
 (* add constants *)
@@ -425,7 +434,7 @@
   in
     thy
     |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
-    |> syntax true Syntax.mode_default (map #2 args)
+    |> syntax ctxt true Syntax.mode_default (map #2 args)
     |> pair (map #3 args)
   end;
 
@@ -493,20 +502,20 @@
 
 in
 
-fun parse_ast_translation atrs = map_syn (Syntax.update_trfuns (mk atrs, [], [], []));
-fun parse_translation trs = map_syn (Syntax.update_trfuns ([], mk trs, [], []));
+fun parse_ast_translation atrs = update_syn_global Syntax.update_trfuns (mk atrs, [], [], []);
+fun parse_translation trs = update_syn_global Syntax.update_trfuns ([], mk trs, [], []);
 fun print_translation tr's =
-  map_syn (Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), []));
-fun typed_print_translation tr's = map_syn (Syntax.update_trfuns ([], [], mk tr's, []));
-fun print_ast_translation atr's = map_syn (Syntax.update_trfuns ([], [], [], mk atr's));
+  update_syn_global Syntax.update_trfuns ([], [], mk (map (apsnd Syntax_Trans.non_typed_tr') tr's), []);
+fun typed_print_translation tr's = update_syn_global Syntax.update_trfuns ([], [], mk tr's, []);
+fun print_ast_translation atr's = update_syn_global Syntax.update_trfuns ([], [], [], mk atr's);
 
 end;
 
 
 (* translation rules *)
 
-val add_trrules = map_syn o Syntax.update_trrules;
-val del_trrules = map_syn o Syntax.remove_trrules;
+val add_trrules = update_syn_global Syntax.update_trrules;
+val del_trrules = update_syn_global Syntax.remove_trrules;
 
 
 (* naming *)