# HG changeset patch
# User wenzelm
# Date 1727721059 -7200
# Node ID dd59daa3c37a88430595f9a989596da14fe91bad
# Parent  83596aea48cb59a88a6903e6f7ccd4264862c7bf
clarified inner-syntax markup, notably for enumerations: prefer "notation=mixfix" over "entity" via 'syntax_consts' (see also 70076ba563d2);

diff -r 83596aea48cb -r dd59daa3c37a NEWS
--- a/NEWS	Mon Sep 30 13:00:42 2024 +0200
+++ b/NEWS	Mon Sep 30 20:30:59 2024 +0200
@@ -28,14 +28,6 @@
 
 *** HOL ***
 
-* Enumerations for tuples, sets, lists etc. now use specific grammar
-productions and separate syntax constants: this allows PIDE markup
-(hyperlinks) for the separators (commas). For example, instead of
-generic nonterminal "args" and syntax constant "_args" from Pure, HOL
-lists now use nonterminal "list_args" and syntax constant "_list_args".
-Rare INCOMPATIBILITY for ambitious syntax translations and grammar
-modifications (e.g. via 'no_syntax').
-
 * Theory "HOL.Wellfounded":
   - Removed lemma wellorder.wfP_less. Use wellorder.wfp_on_less instead.
     Minor INCOMPATIBILITIES.
diff -r 83596aea48cb -r dd59daa3c37a src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -27,12 +27,12 @@
          | Crypt  key msg
 
 syntax
-  "_MTuple"      :: "['a, args] => 'a * 'b"       ("(2\<lbrace>_,/ _\<rbrace>)")
+  "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
 syntax_consts
-  "_MTuple"     == MPair
+  MPair
 translations
-  "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
-  "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
 
 inductive_set
   parts :: "msg set => msg set"
diff -r 83596aea48cb -r dd59daa3c37a src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -452,8 +452,11 @@
 \noindent
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
-
-    syntax "_list" :: "list_args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
+(*<*)
+no_syntax
+  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+(*>*)
+    syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
 
 text \<open>\blankline\<close>
 
diff -r 83596aea48cb -r dd59daa3c37a src/Doc/Tutorial/Protocol/Message.thy
--- a/src/Doc/Tutorial/Protocol/Message.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/Doc/Tutorial/Protocol/Message.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -79,13 +79,10 @@
 
 (*<*)
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
-nonterminal mtuple_args
 syntax
-  "" :: "'a \<Rightarrow> mtuple_args"  ("_")
-  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  ("_,/ _")
-  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  ("(2\<lbrace>_,/ _\<rbrace>)")
+  "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)")
 syntax_consts
-  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
+  MPair
 translations
   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Auth/Message.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -49,13 +49,10 @@
 
 
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
-nonterminal mtuple_args
 syntax
-  "" :: "'a \<Rightarrow> mtuple_args"  (\<open>_\<close>)
-  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  (\<open>_,/ _\<close>)
-  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  (\<open>(2\<lbrace>_,/ _\<rbrace>)\<close>)
+  "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
 syntax_consts
-  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
+  MPair
 translations
   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Codegenerator_Test/Code_Lazy_Test.thy
--- a/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Codegenerator_Test/Code_Lazy_Test.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -23,13 +23,10 @@
 code_lazy_type llist
 
 no_notation lazy_llist (\<open>_\<close>)
-nonterminal llist_args
 syntax
-  "" :: "'a \<Rightarrow> llist_args"  (\<open>_\<close>)
-  "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  (\<open>_,/ _\<close>)
-  "_llist" :: "llist_args => 'a list"    (\<open>\<^bold>[(_)\<^bold>]\<close>)
+  "_llist" :: "args => 'a list"    (\<open>\<^bold>[(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>]\<close>)
 syntax_consts
-  "_llist_args" "_llist" == lazy_llist
+  lazy_llist
 translations
   "\<^bold>[x, xs\<^bold>]" == "x\<^bold>#\<^bold>[xs\<^bold>]"
   "\<^bold>[x\<^bold>]" == "x\<^bold>#\<^bold>[\<^bold>]"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -348,13 +348,10 @@
 
 subsection \<open>List-style syntax for polynomials\<close>
 
-nonterminal poly_args
 syntax
-  "" :: "'a \<Rightarrow> poly_args"  (\<open>_\<close>)
-  "_poly_args" :: "'a \<Rightarrow> poly_args \<Rightarrow> poly_args"  (\<open>_,/ _\<close>)
-  "_poly" :: "poly_args \<Rightarrow> 'a poly"  (\<open>[:(_):]\<close>)
+  "_poly" :: "args \<Rightarrow> 'a poly"  (\<open>[:(\<open>notation=\<open>mixfix polynomial enumeration\<close>\<close>_):]\<close>)
 syntax_consts
-  "_poly_args" "_poly" \<rightleftharpoons> pCons
+  pCons
 translations
   "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
   "[:x:]" \<rightleftharpoons> "CONST pCons x 0"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/HOLCF/IOA/Sequence.thy
--- a/src/HOL/HOLCF/IOA/Sequence.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/HOLCF/IOA/Sequence.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -69,14 +69,11 @@
 
 subsection \<open>List enumeration\<close>
 
-nonterminal llist_args
 syntax
-  "" :: "'a \<Rightarrow> llist_args"  (\<open>_\<close>)
-  "_list_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  (\<open>_,/ _\<close>)
-  "_totlist" :: "llist_args \<Rightarrow> 'a Seq"  (\<open>[(_)!]\<close>)
-  "_partlist" :: "llist_args \<Rightarrow> 'a Seq"  (\<open>[(_)?]\<close>)
+  "_totlist" :: "args \<Rightarrow> 'a Seq"  (\<open>[(\<open>notation=\<open>mixfix total list enumeration\<close>\<close>_)!]\<close>)
+  "_partlist" :: "args \<Rightarrow> 'a Seq"  (\<open>[(\<open>notation=\<open>mixfix partial list enumeration\<close>\<close>_)?]\<close>)
 syntax_consts
-  "_totlist" "_partlist" \<rightleftharpoons> Consq
+  Consq
 translations
   "[x, xs!]" \<rightleftharpoons> "x \<leadsto> [xs!]"
   "[x!]" \<rightleftharpoons> "x\<leadsto>nil"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/HOLCF/Sprod.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -40,13 +40,10 @@
 definition ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c"
   where "ssplit = (\<Lambda> f p. seq\<cdot>p\<cdot>(f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
 
-nonterminal stuple_args
 syntax
-  "" :: "logic \<Rightarrow> stuple_args"  (\<open>_\<close>)
-  "_stuple_args" :: "logic \<Rightarrow> stuple_args \<Rightarrow> stuple_args"  (\<open>_,/ _\<close>)
-  "_stuple" :: "[logic, stuple_args] \<Rightarrow> logic"  (\<open>(1'(:_,/ _:'))\<close>)
+  "_stuple" :: "[logic, args] \<Rightarrow> logic"  (\<open>(\<open>indent=1 notation=\<open>mixfix strict tuple\<close>\<close>'(:_,/ _:'))\<close>)
 syntax_consts
-  "_stuple_args" "_stuple" \<rightleftharpoons> spair
+  spair
 translations
   "(:x, y, z:)" \<rightleftharpoons> "(:x, (:y, z:):)"
   "(:x, y:)" \<rightleftharpoons> "CONST spair\<cdot>x\<cdot>y"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -164,13 +164,10 @@
 lift_definition finsert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is insert parametric Lifting_Set.insert_transfer
   by simp
 
-nonterminal fset_args
 syntax
-  "" :: "'a \<Rightarrow> fset_args"  (\<open>_\<close>)
-  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  (\<open>_,/ _\<close>)
-  "_fset" :: "fset_args => 'a fset"  (\<open>{|(_)|}\<close>)
+  "_fset" :: "args => 'a fset"  (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
 syntax_consts
-  "_fset_args" "_fset" == finsert
+  finsert
 translations
   "{|x, xs|}" == "CONST finsert x {|xs|}"
   "{|x|}"     == "CONST finsert x {||}"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -91,13 +91,10 @@
   "\<lambda>a M b. if b = a then Suc (M b) else M b"
 by (rule add_mset_in_multiset)
 
-nonterminal multiset_args
 syntax
-  "" :: "'a \<Rightarrow> multiset_args"  (\<open>_\<close>)
-  "_multiset_args" :: "'a \<Rightarrow> multiset_args \<Rightarrow> multiset_args"  (\<open>_,/ _\<close>)
-  "_multiset" :: "multiset_args \<Rightarrow> 'a multiset"    (\<open>{#(_)#}\<close>)
+  "_multiset" :: "args \<Rightarrow> 'a multiset"    (\<open>{#(\<open>notation=\<open>mixfix multiset enumeration\<close>\<close>_)#}\<close>)
 syntax_consts
-  "_multiset_args" "_multiset" == add_mset
+  add_mset
 translations
   "{#x, xs#}" == "CONST add_mset x {#xs#}"
   "{#x#}" == "CONST add_mset x {#}"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/List.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -45,13 +45,10 @@
 
 text \<open>List enumeration\<close>
 
-nonterminal list_args
 syntax
-  "" :: "'a \<Rightarrow> list_args"  (\<open>_\<close>)
-  "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args"  (\<open>_,/ _\<close>)
-  "_list" :: "list_args => 'a list"    (\<open>[(_)]\<close>)
+  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
 syntax_consts
-  "_list_args" "_list" == Cons
+  Cons
 translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -48,13 +48,10 @@
 
 
 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close>
-nonterminal mtuple_args
 syntax
-  "" :: "'a \<Rightarrow> mtuple_args"  (\<open>_\<close>)
-  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  (\<open>_,/ _\<close>)
-  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  (\<open>(2\<lbrace>_,/ _\<rbrace>)\<close>)
+  "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
 syntax_consts
-  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
+  MPair
 translations
   "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
   "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Prolog/Test.thy
--- a/src/HOL/Prolog/Test.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Prolog/Test.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -18,13 +18,10 @@
 
 text \<open>List enumeration\<close>
 
-nonterminal list_args
 syntax
-  "" :: "'a \<Rightarrow> list_args"  (\<open>_\<close>)
-  "_list_args" :: "'a \<Rightarrow> list_args \<Rightarrow> list_args"  (\<open>_,/ _\<close>)
-  "_list" :: "list_args => 'a list"    (\<open>[(_)]\<close>)
+  "_list" :: "args => 'a list"    (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
 syntax_consts
-  "_list_args" "_list" == Cons
+  Cons
 translations
   "[x, xs]" == "x#[xs]"
   "[x]" == "x#[]"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Quotient_Examples/Lift_FSet.thy
--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -95,13 +95,10 @@
 
 end
 
-nonterminal fset_args
 syntax
-  "" :: "'a \<Rightarrow> fset_args"  (\<open>_\<close>)
-  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  (\<open>_,/ _\<close>)
-  "_fset" :: "fset_args => 'a fset"  (\<open>{|(_)|}\<close>)
+  "_fset" :: "args => 'a fset"  (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
 syntax_consts
-  "_fset_args" "_fset" == fcons
+  fcons
 translations
   "{|x, xs|}" == "CONST fcons x {|xs|}"
   "{|x|}"     == "CONST fcons x {||}"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Quotient_Examples/Quotient_FSet.thy
--- a/src/HOL/Quotient_Examples/Quotient_FSet.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Quotient_Examples/Quotient_FSet.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -288,13 +288,10 @@
   "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
   is "Cons" by auto
 
-nonterminal fset_args
 syntax
-  "" :: "'a \<Rightarrow> fset_args"  (\<open>_\<close>)
-  "_fset_args" :: "'a \<Rightarrow> fset_args \<Rightarrow> fset_args"  (\<open>_,/ _\<close>)
-  "_fset" :: "fset_args => 'a fset"  (\<open>{|(_)|}\<close>)
+  "_fset" :: "args => 'a fset"  (\<open>{|(\<open>notation=\<open>mixfix finite set enumeration\<close>\<close>_)|}\<close>)
 syntax_consts
-  "_fset_args" "_fset" == insert_fset
+  insert_fset
 translations
   "{|x, xs|}" == "CONST insert_fset x {|xs|}"
   "{|x|}"     == "CONST insert_fset x {||}"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -68,16 +68,13 @@
 
 
 (*Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...*)
-nonterminal mtuple_args
 syntax
-  "" :: "'a \<Rightarrow> mtuple_args"  (\<open>_\<close>)
-  "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args"  (\<open>_,/ _\<close>)
-  "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b"  (\<open>(2\<lbrace>_,/ _\<rbrace>)\<close>)
+  "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b"  (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>)
 syntax_consts
-  "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair
+  MPair
 translations
-  "\<lbrace>x, y, z\<rbrace>"   == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
-  "\<lbrace>x, y\<rbrace>"      == "CONST MPair x y"
+  "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>"
+  "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y"
 
 
 definition nat_of_agent :: "agent \<Rightarrow> nat" where
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Set.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -143,13 +143,10 @@
 definition insert :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set"
   where insert_compr: "insert a B = {x. x = a \<or> x \<in> B}"
 
-nonterminal finset_args
 syntax
-  "" :: "'a \<Rightarrow> finset_args"  (\<open>_\<close>)
-  "_Finset_args" :: "'a \<Rightarrow> finset_args \<Rightarrow> finset_args"  (\<open>_,/ _\<close>)
-  "_Finset" :: "finset_args \<Rightarrow> 'a set"    (\<open>{(_)}\<close>)
+  "_Finset" :: "args \<Rightarrow> 'a set"    (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
 syntax_consts
-  "_Finset_args" "_Finset" \<rightleftharpoons> insert
+  insert
 translations
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/Tools/string_syntax.ML
--- a/src/HOL/Tools/string_syntax.ML	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/Tools/string_syntax.ML	Mon Sep 30 20:30:59 2024 +0200
@@ -123,7 +123,7 @@
 
 fun list_ast_tr' [args] =
       Ast.Appl [Ast.Constant \<^syntax_const>\<open>_String\<close>,
-        (mk_string_ast o maps dest_char_ast o Ast.unfold_ast \<^syntax_const>\<open>_list_args\<close>) args]
+        (mk_string_ast o maps dest_char_ast o Ast.unfold_ast \<^syntax_const>\<open>_args\<close>) args]
   | list_ast_tr' _ = raise Match;
 
 
diff -r 83596aea48cb -r dd59daa3c37a src/HOL/ex/Code_Lazy_Demo.thy
--- a/src/HOL/ex/Code_Lazy_Demo.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -39,13 +39,10 @@
   = LNil (\<open>\<^bold>\<lbrakk>\<^bold>\<rbrakk>\<close>) 
   | LCons (lhd: 'a) (ltl: "'a llist") (infixr \<open>###\<close> 65)
 
-nonterminal llist_args
 syntax
-  "" :: "'a \<Rightarrow> llist_args"  (\<open>_\<close>)
-  "_llist_args" :: "'a \<Rightarrow> llist_args \<Rightarrow> llist_args"  (\<open>_,/ _\<close>)
-  "_llist" :: "llist_args => 'a list"    (\<open>\<^bold>\<lbrakk>(_)\<^bold>\<rbrakk>\<close>)
+  "_llist" :: "args => 'a list"    (\<open>\<^bold>\<lbrakk>(\<open>notation=\<open>mixfix lazy list enumeration\<close>\<close>_)\<^bold>\<rbrakk>\<close>)
 syntax_consts
-  "_llist_args" "_llist" == LCons
+  LCons
 translations
   "\<^bold>\<lbrakk>x, xs\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>xs\<^bold>\<rbrakk>"
   "\<^bold>\<lbrakk>x\<^bold>\<rbrakk>" == "x###\<^bold>\<lbrakk>\<^bold>\<rbrakk>"
diff -r 83596aea48cb -r dd59daa3c37a src/ZF/List.thy
--- a/src/ZF/List.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/ZF/List.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -15,11 +15,8 @@
 
 notation Nil (\<open>[]\<close>)
 
-nonterminal list_args
 syntax
-  "" :: "i \<Rightarrow> list_args"  (\<open>_\<close>)
-  "_List_args" :: "[i, list_args] \<Rightarrow> list_args"  (\<open>_,/ _\<close>)
-  "_List" :: "list_args \<Rightarrow> i"  (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
+  "_List" :: "is \<Rightarrow> i"  (\<open>[(\<open>notation=\<open>mixfix list enumeration\<close>\<close>_)]\<close>)
 syntax_consts
   Cons
 translations
diff -r 83596aea48cb -r dd59daa3c37a src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Mon Sep 30 13:00:42 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Mon Sep 30 20:30:59 2024 +0200
@@ -129,11 +129,11 @@
 definition succ :: "i \<Rightarrow> i"
   where "succ(i) \<equiv> cons(i, i)"
 
-nonterminal "finset_args"
+nonterminal "is"
 syntax
-  "" :: "i \<Rightarrow> finset_args"  (\<open>_\<close>)
-  "_Finset_args" :: "[i, finset_args] \<Rightarrow> finset_args"  (\<open>_,/ _\<close>)
-  "_Finset" :: "finset_args \<Rightarrow> i"  (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
+  "" :: "i \<Rightarrow> is"  (\<open>_\<close>)
+  "_Enum" :: "[i, is] \<Rightarrow> is"  (\<open>_,/ _\<close>)
+  "_Finset" :: "is \<Rightarrow> i"  (\<open>{(\<open>notation=\<open>mixfix set enumeration\<close>\<close>_)}\<close>)
 syntax_consts
   cons
 translations