# HG changeset patch
# User haftmann
# Date 1648533967 -7200
# Node ID 4b8da5eef9d0b3d061242762b89a6ff5468b3d03
# Parent  f9c758208298f00d60f72ac605abf637989a1243
regenerated

diff -r f9c758208298 -r 4b8da5eef9d0 src/HOL/Tools/Qelim/cooper_procedure.ML
--- a/src/HOL/Tools/Qelim/cooper_procedure.ML	Tue Mar 29 06:02:17 2022 +0000
+++ b/src/HOL/Tools/Qelim/cooper_procedure.ML	Tue Mar 29 08:06:07 2022 +0200
@@ -1815,39 +1815,32 @@
       else (zero_inta, Bound n))
   | zsplit0 (CN (n, i, a)) =
     let
-      val aa = zsplit0 a;
-      val (ia, ab) = aa;
+      val (ia, aa) = zsplit0 a;
     in
-      (if equal_nat n zero_nat then (plus_inta i ia, ab)
-        else (ia, CN (n, i, ab)))
+      (if equal_nat n zero_nat then (plus_inta i ia, aa)
+        else (ia, CN (n, i, aa)))
     end
   | zsplit0 (Neg a) = let
-                        val aa = zsplit0 a;
-                        val (i, ab) = aa;
+                        val (i, aa) = zsplit0 a;
                       in
-                        (uminus_int i, Neg ab)
+                        (uminus_int i, Neg aa)
                       end
   | zsplit0 (Add (a, b)) = let
-                             val aa = zsplit0 a;
-                             val (ia, ab) = aa;
-                             val ba = zsplit0 b;
-                             val (ib, bb) = ba;
+                             val (ia, aa) = zsplit0 a;
+                             val (ib, ba) = zsplit0 b;
                            in
-                             (plus_inta ia ib, Add (ab, bb))
+                             (plus_inta ia ib, Add (aa, ba))
                            end
   | zsplit0 (Sub (a, b)) = let
-                             val aa = zsplit0 a;
-                             val (ia, ab) = aa;
-                             val ba = zsplit0 b;
-                             val (ib, bb) = ba;
+                             val (ia, aa) = zsplit0 a;
+                             val (ib, ba) = zsplit0 b;
                            in
-                             (minus_inta ia ib, Sub (ab, bb))
+                             (minus_inta ia ib, Sub (aa, ba))
                            end
   | zsplit0 (Mul (i, a)) = let
-                             val aa = zsplit0 a;
-                             val (ia, ab) = aa;
+                             val (ia, aa) = zsplit0 a;
                            in
-                             (times_inta i ia, Mul (i, ab))
+                             (times_inta i ia, Mul (i, aa))
                            end;
 
 fun zlfm (And (p, q)) = And (zlfm p, zlfm q)