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