--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy Fri Oct 18 15:36:42 2024 +0200
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy Fri Oct 18 15:42:31 2024 +0200
@@ -51,11 +51,11 @@
"mk_word_aux k = exec {
i \<leftarrow> Random.range 10;
(if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
- else exec {
- let l = (if i mod 2 = 0 then A else B);
- ls \<leftarrow> mk_word_aux (Suc k);
- Pair (l # ls)
- })}"
+ else exec {
+ let l = (if i mod 2 = 0 then A else B);
+ ls \<leftarrow> mk_word_aux (Suc k);
+ Pair (l # ls)
+ })}"
by pat_completeness auto
termination
by (relation "measure ((-) 1001)") auto