# HG changeset patch
# User haftmann
# Date 1674843398 -3600
# Node ID 4c4d40913900051baae4220c141b61e42666f28e
# Parent  5ef443fa4a5df356d8b668e256090f4b5a35c746
Restored antiquotation.

diff -r 5ef443fa4a5d -r 4c4d40913900 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Thu Jan 26 15:18:55 2023 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy	Fri Jan 27 19:16:38 2023 +0100
@@ -11,7 +11,7 @@
 
 text \<open>
 We provide a convenient do-notation for monadic expressions well-known from Haskell.
-const>\<open>Let\<close> is printed specially in do-expressions.
+\<^const>\<open>Let\<close> is printed specially in do-expressions.
 \<close>
 
 consts