diff -r 8dc9453889ca -r b57996a0688c src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Sat Dec 07 23:08:51 2024 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sat Dec 07 23:50:18 2024 +0100
@@ -71,7 +71,7 @@
         (case args of
           [(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ Free (s, _) $ p] =>
             (case Term_Position.decode_position1 p of
-              SOME pos => c $ mk_string (content (s, pos)) $ p
+              SOME {pos, ...} => c $ mk_string (content (s, pos)) $ p
             | NONE => err ())
         | _ => err ())
       end;