# 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 \ range ?f" by simp next fix x and f::"'a \\<^sub>F nat" - show "\I S. (\' i\domain f. from_nat_into local.basis_proj ((f)\<^sub>F i)) = Pi' I S \ - finite I \ (\i\I. S i \ local.basis_proj)" + show "\I S. (\' i\domain f. from_nat_into basis_proj ((f)\<^sub>F i)) = Pi' I S \ + finite I \ (\i\I. S i \ basis_proj)" using assms by (auto intro: from_nat_into) qed