src/HOL/Groebner_Basis.thy

 
 use "Tools/Groebner_Basis/normalizer.ML"
 
 
 method_setup sring_norm = {*
-  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
+  Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
 *} "semiring normalizer"
 
 
 locale gb_field = gb_ring +
   fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"

 in
 fn src => Method.syntax 
     ((Scan.optional (keyword addN |-- thms) []) -- 
     (Scan.optional (keyword delN |-- thms) [])) src 
  #> (fn ((add_ths, del_ths), ctxt) => 
-       Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
+       SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
 end
 *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
 declare dvd_def[algebra]
 declare dvd_eq_mod_eq_0[symmetric, algebra]
 declare mod_div_trivial[algebra]