
diff -r 9e71155e3666 -r 0135a0c77b64 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -2661,11 +2661,14 @@
   shows "\<exists>x\<in>A. poly p b - poly p a = (b - a) * poly (pderiv p) x"
 proof (cases a b rule: linorder_cases)
   case less
-  from poly_MVT[OF less, of p] guess x by (elim exE conjE)
+  from poly_MVT[OF less, of p] obtain x
+    where "a < x" "x < b" "poly p b - poly p a = (b - a) * poly (pderiv p) x"
+    by auto
   then show ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms])
 next
   case greater
-  from poly_MVT[OF greater, of p] guess x by (elim exE conjE)
+  from poly_MVT[OF greater, of p] obtain x
+    where "b < x" "x < a" "poly p a - poly p b = (a - b) * poly (pderiv p) x" by auto
   then show ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms])
 qed (use assms in auto)
 




