--- a/src/HOL/Analysis/Polytope.thy Wed May 02 12:48:08 2018 +0100
+++ b/src/HOL/Analysis/Polytope.thy Wed May 02 23:32:47 2018 +0100
@@ -1189,7 +1189,7 @@
qed
then have "dim (S \<inter> {x. a \<bullet> x = 0}) < n"
by (metis (no_types) less_ay c subsetD dim_eq_span inf.strict_order_iff
- inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_clauses(1))
+ inf_le1 \<open>dim S = n\<close> not_le rel_interior_subset span_0 span_superset)
then have "0 \<in> convex hull {x. x extreme_point_of (S \<inter> {x. a \<bullet> x = 0})}"
by (rule less.IH) (auto simp: co less.prems)
then show ?thesis