--- a/src/HOL/Library/Topology_Euclidean_Space.thy Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Mar 16 18:24:30 2009 +0100
@@ -978,9 +978,8 @@
val ss1 = HOL_basic_ss addsimps [@{thm expand_fun_eq} RS sym]
val ss2 = HOL_basic_ss addsimps [@{thm mknet_inverse'}]
fun tac ths = ObjectLogic.full_atomize_tac THEN' Simplifier.simp_tac (ss1 addsimps ths) THEN' Simplifier.asm_full_simp_tac ss2
- in Method.thms_args (SIMPLE_METHOD' o tac) end
-
-*} "Reduces goals about net"
+ in Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (tac ths))) end
+*} "reduces goals about net"
lemma at: "\<And>x y. netord (at a) x y \<longleftrightarrow> 0 < dist x a \<and> dist x a <= dist y a"
apply (net at_def)