# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1503655803 -3600
# Node ID 678774070c9b6423d172c1dc893c981c3c404df2
# Parent  c1d8ab323d858b5cc938c3eede56e0313ac7a61b
renamed s to S to work with previous change

diff -r c1d8ab323d85 -r 678774070c9b src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Aug 24 23:04:47 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Aug 25 11:10:03 2017 +0100
@@ -1347,7 +1347,7 @@
             has_integral  contour_integral (subpath u v g) f) {u..v}"
   using assms
   apply (auto simp: has_integral_integrable_integral)
-  apply (rule integrable_on_subcbox [where a=u and b=v and s = "{0..1}", simplified])
+  apply (rule integrable_on_subcbox [where a=u and b=v and S = "{0..1}", simplified])
   apply (auto simp: contour_integral_unique [OF has_contour_integral_subpath] contour_integrable_on)
   done
 
@@ -1364,7 +1364,7 @@
            contour_integral (subpath u w g) f"
   using assms apply (auto simp: contour_integral_subcontour_integral)
   apply (rule integral_combine, auto)
-  apply (rule integrable_on_subcbox [where a=u and b=w and s = "{0..1}", simplified])
+  apply (rule integrable_on_subcbox [where a=u and b=w and S = "{0..1}", simplified])
   apply (auto simp: contour_integrable_on)
   done