# HG changeset patch
# User wenzelm
# Date 1729453718 -7200
# Node ID 7c2745efec69915b5d25dd55450c60c3c5b8acd3
# Parent  d1170873976e045bd24b90d386878439ac79d099
clarified concrete vs. abstract syntax;

diff -r d1170873976e -r 7c2745efec69 src/HOL/ex/Antiquote.thy
--- 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)"