src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
changeset 81706 7beb0cf38292
parent 72671 588c751a5eef
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jan 02 08:37:52 2025 +0100
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Thu Jan 02 08:37:55 2025 +0100
@@ -655,7 +655,7 @@
     return a
   }"
 
-code_reserved SML upto
+code_reserved (SML) upto
 
 definition "example = do {
     a \<leftarrow> Array.of_list ([42, 2, 3, 5, 0, 1705, 8, 3, 15] :: nat list);