diff -r 5976fe402824 -r 34f782641caa src/HOL/Multivariate_Analysis/Fashoda.thy
--- a/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 13 20:20:16 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Fashoda.thy	Sun Sep 13 21:06:58 2015 +0200
@@ -835,13 +835,13 @@
       z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
       z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
     proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
-      case as: 1
+      case prems: 1
       have "pathfinish f \<in> cbox a b"
         using assms(3) pathfinish_in_path_image[of f] by auto 
       then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
         unfolding mem_interval_cart forall_2 by auto
       then have "z$1 \<noteq> pathfinish f$1"
-        using as(2)
+        using prems(2)
         using assms ab
         by (auto simp add: field_simps)
       moreover have "pathstart f \<in> cbox a b"
@@ -851,13 +851,13 @@
         unfolding mem_interval_cart forall_2
         by auto
       then have "z$1 \<noteq> pathstart f$1"
-        using as(2) using assms ab
+        using prems(2) using assms ab
         by (auto simp add: field_simps)
       ultimately have *: "z$2 = a$2 - 2"
-        using as(1)
+        using prems(1)
         by auto
       have "z$1 \<noteq> pathfinish g$1"
-        using as(2)
+        using prems(2)
         using assms ab
         by (auto simp add: field_simps *)
       moreover have "pathstart g \<in> cbox a b"
@@ -865,11 +865,11 @@
         by auto 
       note this[unfolded mem_interval_cart forall_2]
       then have "z$1 \<noteq> pathstart g$1"
-        using as(1)
+        using prems(1)
         using assms ab
         by (auto simp add: field_simps *)
       ultimately have "a $ 2 - 1 \<le> z $ 2 \<and> z $ 2 \<le> b $ 2 + 3 \<or> b $ 2 + 3 \<le> z $ 2 \<and> z $ 2 \<le> a $ 2 - 1"
-        using as(2)
+        using prems(2)
         unfolding * assms
         by (auto simp add: field_simps)
       then show False