# HG changeset patch
# User wenzelm
# Date 1729864120 -7200
# Node ID ff60c3b565da27de06b0a56e14867e28bbb0a4fd
# Parent  1c2be1fca2bda8bd7875c93011e047d357b04b38
obsolete (see a8502d492dde);

diff -r 1c2be1fca2bd -r ff60c3b565da src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Oct 25 15:39:27 2024 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Oct 25 15:48:40 2024 +0200
@@ -612,7 +612,6 @@
   register_config_bool Syntax.ambiguity_warning #>
   register_config_int Syntax.ambiguity_limit #>
   register_config_bool Syntax_Trans.eta_contract #>
-  register_config_bool Syntax_Phases.const_syntax_legacy #>
   register_config_bool Name_Space.names_long #>
   register_config_bool Name_Space.names_short #>
   register_config_bool Name_Space.names_unique #>
diff -r 1c2be1fca2bd -r ff60c3b565da src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Oct 25 15:39:27 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Oct 25 15:48:40 2024 +0200
@@ -15,7 +15,6 @@
     Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
   val term_of_typ: Proof.context -> typ -> term
-  val const_syntax_legacy: bool Config.T
   val print_checks: Proof.context -> unit
   val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
     Context.generic -> Context.generic
@@ -153,8 +152,6 @@
 
 (* parsetree_to_ast *)
 
-val const_syntax_legacy = Config.declare_bool ("const_syntax_legacy", \<^here>) (K false);
-
 fun parsetree_literals (Parser.Markup (_, ts)) = maps parsetree_literals ts
   | parsetree_literals (Parser.Node _) = []
   | parsetree_literals (Parser.Tip tok) =
@@ -224,7 +221,6 @@
             val args = maps asts_of pts;
             fun head () =
               if not (null ps) andalso (Lexicon.is_fixed a orelse Lexicon.is_const a)
-                andalso not (Config.get ctxt const_syntax_legacy)
               then Ast.constrain (Ast.Constant a) (ast_of_pos ps)
               else Ast.Constant a;
             val _ = List.app (fn pos => report pos markup_cache a) ps;