# HG changeset patch
# User wenzelm
# Date 1729630347 -7200
# Node ID a8502d492dde72f1ce7f5ae724ae4c2ee4c3a61d
# Parent  8454a245952ac142d7fecd330607d0f38c22050a
adhoc option to disable const constraints, notably for AFP/Isabelle_DOF;

diff -r 8454a245952a -r a8502d492dde src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Oct 22 22:34:33 2024 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Oct 22 22:52:27 2024 +0200
@@ -612,6 +612,7 @@
   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 8454a245952a -r a8502d492dde src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Oct 22 22:34:33 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Oct 22 22:52:27 2024 +0200
@@ -15,6 +15,7 @@
     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
@@ -152,6 +153,8 @@
 
 (* 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) =
@@ -228,7 +231,8 @@
             val ps = maps parsetree_literals pts;
             val args = maps asts_of pts;
             fun head () =
-              if Lexicon.is_fixed a orelse Lexicon.is_const a
+              if (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;