--- a/src/HOL/Topological_Spaces.thy Mon Jan 11 07:44:20 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy Mon Jan 11 11:56:35 2016 +0100
@@ -2444,8 +2444,9 @@
end
lemma uniformity_Abort:
- "uniformity = Abs_filter (\<lambda>P. Code.abort (STR ''uniformity is not executable'') (\<lambda>x. Rep_filter uniformity P))"
- unfolding Code.abort_def Rep_filter_inverse ..
+ "uniformity =
+ Filter.abstract_filter (\<lambda>u. Code.abort (STR ''uniformity is not executable'') (\<lambda>u. uniformity))"
+ by simp
class open_uniformity = "open" + uniformity +
assumes open_uniformity: "\<And>U. open U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"