diff -r 1c50ddcf6a01 -r 7dbac7d3cdab src/HOL/Examples/Rewrite_Examples.thy
--- a/src/HOL/Examples/Rewrite_Examples.thy	Thu Dec 09 08:32:29 2021 +0100
+++ b/src/HOL/Examples/Rewrite_Examples.thy	Thu Dec 09 09:40:15 2021 +0100
@@ -268,7 +268,7 @@
   val th = Rewrite.rewrite_conv ctxt (pat, to) @{thms add.commute} ct
 \<close>
 
-section \<open>Regression tests\<close>
+text \<open>Some regression tests\<close>
 
 ML \<open>
   val ct = \<^cterm>\<open>(\<lambda>b :: int. (\<lambda>a. b + a))\<close>