# HG changeset patch
# User wenzelm
# Date 1395267225 -3600
# Node ID 6599c627854544640bf07b88d6866c5b4fbe9fc6
# Parent  a8dfbe9f25daeee07f8b354ceb4454dabe3307de
tuned -- no need for slightly obscure "local" prefix;

diff -r a8dfbe9f25da -r 6599c6278545 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Wed Mar 19 22:26:27 2014 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Wed Mar 19 23:13:45 2014 +0100
@@ -545,8 +545,8 @@
   thus "Pi' I S \<in> range ?f" by simp
 next
   fix x and f::"'a \<Rightarrow>\<^sub>F nat"
-  show "\<exists>I S. (\<Pi>' i\<in>domain f. from_nat_into local.basis_proj ((f)\<^sub>F i)) = Pi' I S \<and>
-    finite I \<and> (\<forall>i\<in>I. S i \<in> local.basis_proj)"
+  show "\<exists>I S. (\<Pi>' i\<in>domain f. from_nat_into basis_proj ((f)\<^sub>F i)) = Pi' I S \<and>
+    finite I \<and> (\<forall>i\<in>I. S i \<in> basis_proj)"
     using assms by (auto intro: from_nat_into)
 qed