clarified concrete vs. abstract syntax;

--- a/src/HOL/ex/Antiquote.thy	Sun Oct 20 20:32:53 2024 +0200
+++ b/src/HOL/ex/Antiquote.thy	Sun Oct 20 21:48:38 2024 +0200
@@ -10,22 +10,20 @@
 
 text \<open>A simple example on quote / antiquote in higher-order abstract syntax.\<close>
 
-definition var :: "'a \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"  (\<open>VAR _\<close> [1000] 999)
-  where "var x env = env x"
-
 definition Expr :: "(('a \<Rightarrow> nat) \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
   where "Expr exp env = exp env"
 
 syntax
   "_Expr" :: "'a \<Rightarrow> 'a"  (\<open>EXPR _\<close> [1000] 999)
+  "_Var" :: "'a \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"  (\<open>VAR _\<close> [1000] 999)
 
 parse_translation
   \<open>[Syntax_Trans.quote_antiquote_tr
-    \<^syntax_const>\<open>_Expr\<close> \<^const_syntax>\<open>var\<close> \<^const_syntax>\<open>Expr\<close>]\<close>
+    \<^syntax_const>\<open>_Expr\<close> \<^syntax_const>\<open>_Var\<close> \<^const_syntax>\<open>Expr\<close>]\<close>
 
 print_translation
   \<open>[Syntax_Trans.quote_antiquote_tr'
-    \<^syntax_const>\<open>_Expr\<close> \<^const_syntax>\<open>var\<close> \<^const_syntax>\<open>Expr\<close>]\<close>
+    \<^syntax_const>\<open>_Expr\<close> \<^syntax_const>\<open>_Var\<close> \<^const_syntax>\<open>Expr\<close>]\<close>
 
 term "EXPR (a + b + c)"
 term "EXPR (a + b + c + VAR x + VAR y + 1)"