diff -r d9dd4a9f18fc -r e1576d13e933 src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Thu Apr 12 18:39:19 2012 +0200
@@ -13,7 +13,6 @@
   exception COOPER of string
   val conv: Proof.context -> conv
   val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
-  val method: (Proof.context -> Method.method) context_parser
   val setup: theory -> theory
 end;
 
@@ -857,23 +856,6 @@
   THEN_ALL_NEW finish_tac elim
 end;
 
-val method =
-  let
-    fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ()
-    fun simple_keyword k = Scan.lift (Args.$$$ k) >> K ()
-    val addN = "add"
-    val delN = "del"
-    val elimN = "elim"
-    val any_keyword = keyword addN || keyword delN || simple_keyword elimN
-    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
-  in
-    Scan.optional (simple_keyword elimN >> K false) true --
-    Scan.optional (keyword addN |-- thms) [] --
-    Scan.optional (keyword delN |-- thms) [] >>
-    (fn ((elim, add_ths), del_ths) => fn ctxt =>
-      SIMPLE_METHOD' (tac elim add_ths del_ths ctxt))
-  end;
-
 
 (* theory setup *)