src/HOL/Tools/groebner.ML
changeset 47432 e1576d13e933
parent 46497 89ccf66aa73d
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/groebner.ML	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/Tools/groebner.ML	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -16,7 +16,6 @@
     1.4    val ring_tac: thm list -> thm list -> Proof.context -> int -> tactic
     1.5    val ideal_tac: thm list -> thm list -> Proof.context -> int -> tactic
     1.6    val algebra_tac: thm list -> thm list -> Proof.context -> int -> tactic
     1.7 -  val algebra_method: (Proof.context -> Method.method) context_parser
     1.8  end
     1.9  
    1.10  structure Groebner : GROEBNER =
    1.11 @@ -1027,21 +1026,4 @@
    1.12  fun algebra_tac add_ths del_ths ctxt i =
    1.13   ring_tac add_ths del_ths ctxt i ORELSE ideal_tac add_ths del_ths ctxt i
    1.14  
    1.15 -local
    1.16 -
    1.17 -fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
    1.18 -val addN = "add"
    1.19 -val delN = "del"
    1.20 -val any_keyword = keyword addN || keyword delN
    1.21 -val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    1.22 -
    1.23 -in
    1.24 -
    1.25 -val algebra_method = ((Scan.optional (keyword addN |-- thms) []) --
    1.26 -   (Scan.optional (keyword delN |-- thms) [])) >>
    1.27 -  (fn (add_ths, del_ths) => fn ctxt =>
    1.28 -       SIMPLE_METHOD' (algebra_tac add_ths del_ths ctxt))
    1.29 -
    1.30  end;
    1.31 -
    1.32 -end;