diff -r 4ec8e654112f -r 2865a6618cba src/Doc/Codegen/Foundations.thy
--- a/src/Doc/Codegen/Foundations.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/Doc/Codegen/Foundations.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -273,9 +273,9 @@
     of (Some x, q') \<Rightarrow> (x, q'))"
 
 lemma %quote strict_dequeue_AQueue [code]:
-  "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
   "strict_dequeue (AQueue xs []) =
     (case rev xs of y # ys \<Rightarrow> (y, AQueue [] ys))"
+  "strict_dequeue (AQueue xs (y # ys)) = (y, AQueue xs ys)"
   by (simp_all add: strict_dequeue_def) (cases xs, simp_all split: list.split)
 
 text \<open>