# HG changeset patch
# User wenzelm
# Date 1724591501 -7200
# Node ID db4ac82659f4a0855f6e92df8bd876fcd1d84e5c
# Parent  bc936d3d8b451ead91ccaf08bfa9c846cdc1e907
tuned;

diff -r bc936d3d8b45 -r db4ac82659f4 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Aug 25 15:07:22 2024 +0200
+++ b/src/HOL/HOL.thy	Sun Aug 25 15:11:41 2024 +0200
@@ -188,13 +188,6 @@
       in Syntax.const \<^syntax_const>\<open>_The\<close> $ x $ t end)]
 \<close>  \<comment> \<open>To avoid eta-contraction of body\<close>
 
-nonterminal letbinds and letbind
-syntax
-  "_bind"       :: "[pttrn, 'a] \<Rightarrow> letbind"              ("(2_ =/ _)" 10)
-  ""            :: "letbind \<Rightarrow> letbinds"                 ("_")
-  "_binds"      :: "[letbind, letbinds] \<Rightarrow> letbinds"     ("_;/ _")
-  "_Let"        :: "[letbinds, 'a] \<Rightarrow> 'a"                ("(let (_)/ in (_))" [0, 10] 10)
-
 nonterminal case_syn and cases_syn
 syntax
   "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  ("(case _ of/ _)" 10)
@@ -237,6 +230,12 @@
 definition Let :: "'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
   where "Let s f \<equiv> f s"
 
+nonterminal letbinds and letbind
+syntax
+  "_bind"       :: "[pttrn, 'a] \<Rightarrow> letbind"              ("(2_ =/ _)" 10)
+  ""            :: "letbind \<Rightarrow> letbinds"                 ("_")
+  "_binds"      :: "[letbind, letbinds] \<Rightarrow> letbinds"     ("_;/ _")
+  "_Let"        :: "[letbinds, 'a] \<Rightarrow> 'a"                ("(let (_)/ in (_))" [0, 10] 10)
 syntax_consts
   "_bind" "_binds" "_Let" \<rightleftharpoons> Let
 translations