# HG changeset patch
# User wenzelm
# Date 1729258951 -7200
# Node ID 5036454794a53f53d0ba3544682c282088e80677
# Parent  c5b398584f5e5368e35f5357b5495ee601d51ebe
tuned whitespace;

diff -r c5b398584f5e -r 5036454794a5 src/HOL/Proofs/Extraction/Higman_Extraction.thy
--- 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