# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1525809776 -3600
# Node ID bdb2837399f1ceacb18582cd8b3651ec04bda536
# Parent  a49cf225fc9787e5cb1af9ca9af58c7f73a26398
one tiny fix

diff -r a49cf225fc97 -r bdb2837399f1 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Tue May 08 19:00:17 2018 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Tue May 08 21:02:56 2018 +0100
@@ -203,7 +203,7 @@
   have A_notempty: "\<And>i. i \<in> domain x \<Longrightarrow> A i \<noteq> {}" using open_sub[of _ "\<lambda>_. UNIV"] by auto
   let ?A = "(\<lambda>f. Pi' (domain x) f) ` (Pi\<^sub>E (domain x) A)"
   show "\<exists>A::nat \<Rightarrow> ('a\<Rightarrow>\<^sub>F'b) set. (\<forall>i. x \<in> (A i) \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
-  proof (rule first_countableI[where A="?A"], safe)
+  proof (rule first_countableI[of "?A"], safe)
     show "countable ?A" using A by (simp add: countable_PiE)
   next
     fix S::"('a \<Rightarrow>\<^sub>F 'b) set" assume "open S" "x \<in> S"