# HG changeset patch
# User wenzelm
# Date 1726585537 -7200
# Node ID d0d0d12cd4cc27f20d672af3383a857c41d15d4e
# Parent  2870315eea9e9c00f48c4d22eb2692bf8aa7252b
obsolete --- superseded by Local_Theory.syntax_cmd;

diff -r 2870315eea9e -r d0d0d12cd4cc src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Sep 17 11:32:11 2024 +0200
+++ b/src/Pure/sign.ML	Tue Sep 17 17:05:37 2024 +0200
@@ -77,7 +77,6 @@
   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_cmd: bool -> Syntax.mode -> (string * string * 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
@@ -383,16 +382,12 @@
 
 (* modify syntax *)
 
-fun gen_syntax parse_typ add mode args thy =
+fun syntax add mode args thy =
   let
-    val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
-    fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
+    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;
 
-val syntax = gen_syntax (K I);
-val syntax_cmd = gen_syntax Syntax.read_typ;
-
 val syntax_deps = map_syn o Syntax.update_consts;
 
 fun type_notation add mode args =