# HG changeset patch
# User wenzelm
# Date 1243107662 -7200
# Node ID 2291e4d628eb8a5da7c0cfe27b525c57798f550a
# Parent  5c1aca930404b93d68935b3f553fb2c0d4dc852b
removed some obsolete combinators for method args;

diff -r 5c1aca930404 -r 2291e4d628eb src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sat May 23 21:40:34 2009 +0200
+++ b/src/Pure/Isar/method.ML	Sat May 23 21:41:02 2009 +0200
@@ -85,7 +85,6 @@
     theory -> theory
   val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
   val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
-  val no_args: method -> src -> Proof.context -> method
   type modifier = (Proof.context -> Proof.context) * attribute
   val section: modifier parser list -> thm list context_parser
   val sections: modifier parser list -> thm list list context_parser
@@ -100,12 +99,6 @@
   val thms_ctxt_args: (thm list -> Proof.context -> 'a) -> src -> Proof.context -> 'a
   val thms_args: (thm list -> 'a) -> src -> Proof.context -> 'a
   val thm_args: (thm -> 'a) -> src -> Proof.context -> 'a
-  val goal_args: 'a parser -> ('a -> int -> tactic) -> src -> Proof.context -> method
-  val goal_args': 'a context_parser -> ('a -> int -> tactic) -> src -> Proof.context -> method
-  val goal_args_ctxt: 'a parser -> (Proof.context -> 'a -> int -> tactic) -> src ->
-    Proof.context -> method
-  val goal_args_ctxt': 'a context_parser -> (Proof.context -> 'a -> int -> tactic) -> src ->
-    Proof.context -> method
   val parse: text parser
 end;
 
@@ -426,8 +419,6 @@
 fun ctxt_args (f: Proof.context -> method) src ctxt =
   fst (syntax (Scan.succeed (f ctxt)) src ctxt);
 
-fun no_args m = ctxt_args (K m);
-
 
 (* sections *)
 
@@ -468,20 +459,6 @@
   (fn (n, ths) => K (m n ths));
 
 
-(* tactic syntax *)
-
-fun goal_args' args tac src ctxt = fst (syntax (Args.goal_spec -- args >>
-  (fn (quant, s) => SIMPLE_METHOD'' quant (tac s))) src ctxt);
-
-fun goal_args args tac = goal_args' (Scan.lift args) tac;
-
-fun goal_args_ctxt' args tac src ctxt =
-  fst (syntax (Args.goal_spec -- args >>
-  (fn (quant, s) => SIMPLE_METHOD'' quant (tac ctxt s))) src ctxt);
-
-fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
-
-
 (* outer parser *)
 
 fun is_symid_meth s =