allow to specify suffix of goal parameters;

--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 02 00:09:04 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 02 12:33:04 2015 +0200
@@ -688,7 +688,11 @@
     Attrib.empty_binding;
 
 val for_params =
-  Scan.optional (@{keyword "for"} |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.name))) [];
+  Scan.optional
+    (@{keyword "for"} |--
+      Parse.!!! ((Scan.option Parse.dots >> is_some) --
+        (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
+    (false, []);
 
 in
 

--- a/src/Pure/Isar/parse.ML	Thu Jul 02 00:09:04 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Thu Jul 02 12:33:04 2015 +0200
@@ -23,6 +23,7 @@
   val short_ident: string parser
   val long_ident: string parser
   val sym_ident: string parser
+  val dots: string parser
   val minus: string parser
   val term_var: string parser
   val type_ident: string parser
@@ -220,7 +221,10 @@
   group (fn () => "reserved identifier " ^ quote x)
     (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
 
+val dots = sym_ident :-- (fn "\\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
+
 val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
+
 val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
 fun maybe scan = underscore >> K NONE || scan >> SOME;
 

--- a/src/Pure/Isar/proof_context.ML	Thu Jul 02 00:09:04 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Jul 02 12:33:04 2015 +0200
@@ -1241,7 +1241,7 @@
 
 val apply_case = apfst fst oo case_result;
 
-fun check_case ctxt internal (name, pos) fxs =
+fun check_case ctxt internal (name, pos) param_specs =
   let
     val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, {legacy}), _)) =
       Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
@@ -1251,12 +1251,12 @@
           " -- use proof method \"goals\" instead")
       else ();
 
-    val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) fxs;
+    val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs;
     fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
       | replace [] ys = ys
       | replace (_ :: _) [] =
           error ("Too many parameters for case " ^ quote name ^ Position.here pos);
-    val fixes' = replace fxs fixes;
+    val fixes' = replace param_specs fixes;
     val binds' = map drop_schematic binds;
   in
     if null (fold (Term.add_tvarsT o snd) fixes []) andalso

--- a/src/Pure/subgoal.ML	Thu Jul 02 00:09:04 2015 +0200
+++ b/src/Pure/subgoal.ML	Thu Jul 02 12:33:04 2015 +0200
@@ -25,10 +25,10 @@
   val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
   val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
   val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
-  val subgoal: Attrib.binding -> Attrib.binding option -> string option list ->
-    Proof.state -> focus * Proof.state
-  val subgoal_cmd: Attrib.binding -> Attrib.binding option -> string option list ->
-    Proof.state -> focus * Proof.state
+  val subgoal: Attrib.binding -> Attrib.binding option ->
+    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
+  val subgoal_cmd: Attrib.binding -> Attrib.binding option ->
+    bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
 end;
 
 structure Subgoal: SUBGOAL =
@@ -163,30 +163,38 @@
 
 local
 
-fun rename_params ctxt param_specs st =
+fun rename_params ctxt (param_suffix, raw_param_specs) st =
   let
     val _ = if Thm.no_prems st then error "No subgoals!" else ();
-    val (A, C) = Logic.dest_implies (Thm.prop_of st);
+    val (subgoal, goal') = Logic.dest_implies (Thm.prop_of st);
+    val subgoal_params =
+      map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
+      |> Term.variant_frees subgoal |> map #1;
 
-    val params =
-      map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars A)
-      |> Term.variant_frees A |> map #1;
+    val n = length subgoal_params;
+    val m = length raw_param_specs;
     val _ =
-      (case drop (length params) param_specs of
-        [] => ()
-      | bad => error ("Excessive subgoal parameters: " ^ commas_quote (map (the_default "_") bad)));
+      m <= n orelse
+        error ("Excessive subgoal parameter specification" ^
+          Position.here_list (map snd (drop n raw_param_specs)));
 
-    fun rename_list (SOME x :: xs) (y :: ys) =
-          (Proof_Context.cert_var (Binding.name x, NONE, NoSyn) ctxt; x :: rename_list xs ys)
-      | rename_list (NONE :: xs) (y :: ys) = y :: rename_list xs ys
+    val param_specs =
+      raw_param_specs |> map
+        (fn (NONE, _) => NONE
+          | (SOME x, pos) =>
+              let val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
+              in SOME (Variable.check_name b) end)
+      |> param_suffix ? append (replicate (n - m) NONE);
+
+    fun rename_list (opt_x :: xs) (y :: ys) = (the_default y opt_x :: rename_list xs ys)
       | rename_list _ ys = ys;
 
     fun rename_prop (x :: xs) ((c as Const ("Pure.all", _)) $ Abs (_, T, t)) =
           (c $ Abs (x, T, rename_prop xs t))
       | rename_prop [] t = t;
-  in
-    Thm.renamed_prop (Logic.mk_implies (rename_prop (rename_list param_specs params) A, C)) st
-  end;
+
+    val subgoal' = rename_prop (rename_list param_specs subgoal_params) subgoal;
+  in Thm.renamed_prop (Logic.mk_implies (subgoal', goal')) st end;
 
 fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
   let