
diff -r 4a2c82644889 -r 21da2a03b9d2 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 18 20:01:59 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 18 20:31:22 2013 +0100
@@ -5445,7 +5445,7 @@
 have *: "S Int closure T = S" using assms by auto
 have "~(rel_interior S <= rel_frontier T)"
      using closure_mono[of "rel_interior S" "rel_frontier T"] closed_rel_frontier[of T]
-     closure_closed convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
+     closure_closed[of S] convex_closure_rel_interior[of S] closure_subset[of S] assms by auto
 hence "(rel_interior S) Int (rel_interior (closure T)) ~= {}"
      using assms rel_frontier_def[of T] rel_interior_subset convex_rel_interior_closure[of T] by auto
 hence "rel_interior S Int rel_interior T = rel_interior (S Int closure T)" using assms convex_closure




