# HG changeset patch
# User wenzelm
# Date 953574427 -3600
# Node ID de307f5bc89ad15e638f138ca3825d6941cc8ded
# Parent  7428194b39f7b8b081161a19d84edaff6ff9a1af
goal_spec;

diff -r 7428194b39f7 -r de307f5bc89a src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Mar 20 18:46:53 2000 +0100
+++ b/src/Pure/Isar/args.ML	Mon Mar 20 18:47:07 2000 +0100
@@ -33,7 +33,8 @@
   val local_term: Proof.context * T list -> term * (Proof.context * T list)
   val local_prop: Proof.context * T list -> term * (Proof.context * T list)
   val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
-  val goal_spec: T list -> ((int -> tactic) -> tactic) * T list
+  val goal_spec: ((int -> tactic) -> tactic) -> ('a * T list)
+    -> ((int -> tactic) -> tactic) * ('a * T list)
   type src
   val src: (string * T list) * Position.T -> src
   val dest_src: src -> (string * T list) * Position.T
@@ -143,10 +144,17 @@
   ($$$ "!" >> K (ProofContext.prems_of ctxt) || Scan.succeed []) >> pair ctxt);
 
 
-(* goal specifier *)
+(* goal specification *)
+
+(* range *)
 
-val tactical = $$$$ "!" >> K ALLGOALS || $$$$ "?" >> K FINDGOAL || nat >> curry op |>;
-val goal_spec = $$$$ "(" |-- tactical --| $$$$ ")";
+val from_to =
+  nat -- ($$$$ "-" |-- nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
+  nat --| $$$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
+  nat >> (fn i => fn tac => tac i);
+
+val goal = $$$$ "[" |-- !!! (from_to --| $$$$ "]");
+fun goal_spec def = Scan.lift (Scan.optional goal def);
 
 
 (* args *)