src/HOL/IMP/Collecting.thy

--- a/src/HOL/IMP/Collecting.thy	Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/IMP/Collecting.thy	Thu Nov 08 09:11:52 2018 +0100
@@ -94,7 +94,7 @@
      dest: size_annos_same)
 
 definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
-"Inf_acom c M = annotate (\<lambda>p. INF C:M. anno C p) c"
+"Inf_acom c M = annotate (\<lambda>p. INF C\<in>M. anno C p) c"
 
 global_interpretation
   Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c