src/HOL/Library/Euclidean_Space.thy

          ORELSE rtac @{thm setsum_0'} i
          ORELSE simp_tac (HOL_basic_ss addsimps [@{thm "Cart_eq"}]) i)
    (* THEN' TRY o clarify_tac HOL_cs  THEN' (TRY o rtac @{thm iffI}) *)
    THEN' asm_full_simp_tac (ss2 addsimps ths)
  in
-  Method.thms_args (Method.SIMPLE_METHOD' o vector_arith_tac)
+  Method.thms_args (SIMPLE_METHOD' o vector_arith_tac)
 end
 *} "Lifts trivial vector statements to real arith statements"
 
 lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
 lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def)

   "x \<noteq> y \<longleftrightarrow> \<not> (norm (x - y) \<le> 0)"
   using norm_ge_zero[of "x - y"] by auto
 
 use "normarith.ML"
 
-method_setup norm = {* Method.ctxt_args (Method.SIMPLE_METHOD' o NormArith.norm_arith_tac)
+method_setup norm = {* Method.ctxt_args (SIMPLE_METHOD' o NormArith.norm_arith_tac)
 *} "Proves simple linear statements about vector norms"
 
 
 
 text{* Hence more metric properties. *}