# HG changeset patch
# User nipkow
# Date 1513800368 -3600
# Node ID 754952c12293f4e439853e0cf283aa4fe115fc1d
# Parent  b2800da9eb8ad129c1a992da417cd9567572312e
tuned op's

diff -r b2800da9eb8a -r 754952c12293 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Dec 20 19:17:37 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Dec 20 21:06:08 2017 +0100
@@ -2158,11 +2158,11 @@
 
 lemma compactE_image:
   assumes "compact S"
-    and op: "\<And>T. T \<in> C \<Longrightarrow> open (f T)"
+    and opn: "\<And>T. T \<in> C \<Longrightarrow> open (f T)"
     and S: "S \<subseteq> (\<Union>c\<in>C. f c)"
   obtains C' where "C' \<subseteq> C" and "finite C'" and "S \<subseteq> (\<Union>c\<in>C'. f c)"
     apply (rule compactE[OF \<open>compact S\<close> S])
-    using op apply force
+    using opn apply force
     by (metis finite_subset_image)
 
 lemma compact_Int_closed [intro]: