
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/NSA/Filter.thy
--- a/src/HOL/NSA/Filter.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/NSA/Filter.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -77,10 +77,9 @@
 apply (simp add: singleton)
 done
 
-lemma (in freeultrafilter) filter: "filter F" by unfold_locales
+lemma (in freeultrafilter) filter: "filter F" ..
 
-lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
-  by unfold_locales
+lemma (in freeultrafilter) ultrafilter: "ultrafilter F" ..
 
 
 subsection {* Collect properties *}




