src/HOL/Groebner_Basis.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 30654 254478a8dd05
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Mar 16 17:51:24 2009 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Mar 16 18:24:30 2009 +0100
     1.3 @@ -253,7 +253,7 @@
     1.4  
     1.5  
     1.6  method_setup sring_norm = {*
     1.7 -  Method.ctxt_args (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
     1.8 +  Scan.succeed (SIMPLE_METHOD' o Normalizer.semiring_normalize_tac)
     1.9  *} "semiring normalizer"
    1.10  
    1.11  
    1.12 @@ -427,10 +427,9 @@
    1.13   val any_keyword = keyword addN || keyword delN
    1.14   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    1.15  in
    1.16 -fn src => Method.syntax 
    1.17 -    ((Scan.optional (keyword addN |-- thms) []) -- 
    1.18 -    (Scan.optional (keyword delN |-- thms) [])) src 
    1.19 - #> (fn ((add_ths, del_ths), ctxt) => 
    1.20 +  ((Scan.optional (keyword addN |-- thms) []) -- 
    1.21 +   (Scan.optional (keyword delN |-- thms) [])) >>
    1.22 +  (fn (add_ths, del_ths) => fn ctxt =>
    1.23         SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
    1.24  end
    1.25  *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"