diff -r be8c0e039a5e -r bc936d3d8b45 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Sun Aug 25 15:02:19 2024 +0200
+++ b/src/CCL/Term.thy	Sun Aug 25 15:07:22 2024 +0200
@@ -49,8 +49,8 @@
   where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
 
 syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
+syntax_consts "_let1" == let1
 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
-syntax_consts "_let1" == let1
 
 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
@@ -68,6 +68,10 @@
   "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
   "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
   "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
+syntax_consts
+  "_letrec" == letrec and
+  "_letrec2" == letrec2 and
+  "_letrec3" == letrec3
 parse_translation \<open>
   let
     fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
@@ -123,10 +127,6 @@
      (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
   end
 \<close>
-syntax_consts
-  "_letrec" == letrec and
-  "_letrec2" == letrec2 and
-  "_letrec3" == letrec3
 
 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"