Variable.focus etc.: optional bindings provided by user;
Subgoal.focus command: more careful treatment of user-provided bindings;

--- a/src/Doc/Implementation/Proof.thy	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/Doc/Implementation/Proof.thy	Wed Jul 08 19:28:43 2015 +0200
@@ -109,7 +109,7 @@
   @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
   @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
   ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\
-  @{index_ML Variable.focus: "term -> Proof.context ->
+  @{index_ML Variable.focus: "binding list option -> term -> Proof.context ->
   ((string * (string * typ)) list * term) * Proof.context"} \\
   \end{mldecls}
 
@@ -153,8 +153,8 @@
   should be accessible to the user, otherwise newly introduced names
   are marked as ``internal'' (\secref{sec:names}).
 
-  \item @{ML Variable.focus}~@{text B} decomposes the outermost @{text
-  "\<And>"} prefix of proposition @{text "B"}.
+  \item @{ML Variable.focus}~@{text "bindings B"} decomposes the outermost @{text
+  "\<And>"} prefix of proposition @{text "B"}, using the given name bindings.
 
   \end{description}
 \<close>
@@ -394,9 +394,12 @@
   Proof.context -> int -> tactic"} \\
   @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) ->
   Proof.context -> int -> tactic"} \\
-  @{index_ML Subgoal.focus: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
-  @{index_ML Subgoal.focus_prems: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
-  @{index_ML Subgoal.focus_params: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
+  @{index_ML Subgoal.focus: "Proof.context -> int -> binding list option ->
+  thm -> Subgoal.focus * thm"} \\
+  @{index_ML Subgoal.focus_prems: "Proof.context -> int -> binding list option ->
+  thm -> Subgoal.focus * thm"} \\
+  @{index_ML Subgoal.focus_params: "Proof.context -> int -> binding list option ->
+  thm -> Subgoal.focus * thm"} \\
   \end{mldecls}
 
   \begin{mldecls}
@@ -473,7 +476,7 @@
     ML_val
      \<open>val {goal, context = goal_ctxt, ...} = @{Isar.goal};
       val (focus as {params, asms, concl, ...}, goal') =
-        Subgoal.focus goal_ctxt 1 goal;
+        Subgoal.focus goal_ctxt 1 (SOME [@{binding x}]) goal;
       val [A, B] = #prems focus;
       val [(_, x)] = #params focus;\<close>
     sorry

--- a/src/HOL/Eisbach/match_method.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -304,7 +304,7 @@
 
 fun prep_fact_pat ((x, args), pat) ctxt =
   let
-    val ((params, pat'), ctxt') = Variable.focus pat ctxt;
+    val ((params, pat'), ctxt') = Variable.focus NONE pat ctxt;
     val params' = map (Free o snd) params;
 
     val morphism =
@@ -500,10 +500,10 @@
 
 
 (* Fix schematics in the goal *)
-fun focus_concl ctxt i goal =
+fun focus_concl ctxt i bindings goal =
   let
     val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
-      Subgoal.focus_params ctxt i goal;
+      Subgoal.focus_params ctxt i bindings goal;
 
     val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
     val (_, schematic_terms) = Thm.certify_inst ctxt'' inst;
@@ -711,7 +711,7 @@
             val (goal_thins, goal) = get_thinned_prems goal;
 
             val ((local_premids, {context = focus_ctxt, params, asms, concl, ...}), focused_goal) =
-              focus_cases (K Subgoal.focus_prems) (focus_concl) ctxt 1 goal
+              focus_cases (K Subgoal.focus_prems) focus_concl ctxt 1 NONE goal
               |>> augment_focus;
 
             val texts =

--- a/src/HOL/Library/Old_SMT/old_smt_solver.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -281,7 +281,7 @@
       |> Config.put Old_SMT_Config.oracle false
       |> Config.put Old_SMT_Config.filter_only_facts true
 
-    val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
+    val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i NONE goal
     fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply
     val cprop =
       (case try negate (Thm.rhs_of (Old_SMT_Normalize.atomize_conv ctxt' concl)) of

--- a/src/HOL/Tools/Function/function_context_tree.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/HOL/Tools/Function/function_context_tree.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -103,7 +103,7 @@
 (* Called on the INSTANTIATED branches of the congruence rule *)
 fun mk_branch ctxt t =
   let
-    val ((params, impl), ctxt') = Variable.focus t ctxt
+    val ((params, impl), ctxt') = Variable.focus NONE t ctxt
     val (assms, concl) = Logic.strip_horn impl
   in
     (ctxt', map #2 params, assms, rhs_of concl)

--- a/src/HOL/Tools/Function/induction_schema.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -53,7 +53,7 @@
 
 fun dest_hhf ctxt t =
   let
-    val ((params, imp), ctxt') = Variable.focus t ctxt
+    val ((params, imp), ctxt') = Variable.focus NONE t ctxt
   in
     (ctxt', map #2 params, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
   end

--- a/src/HOL/Tools/Function/partial_function.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -230,7 +230,7 @@
     val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data;
 
     val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
-    val ((_, plain_eqn), args_ctxt) = Variable.focus eqn lthy;
+    val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy;
 
     val ((f_binding, fT), mixfix) = the_single fixes;
     val fname = Binding.name_of f_binding;

--- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -252,7 +252,7 @@
   let
     val ctxt = ctxt0 |> Config.put SMT_Config.timeout (Time.toReal time_limit)
 
-    val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i goal
+    val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i NONE goal
     fun negate ct = Thm.dest_comb ct ||> Thm.apply @{cterm Not} |-> Thm.apply
     val cprop =
       (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt concl)) of

--- a/src/HOL/ex/Meson_Test.thy	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/HOL/ex/Meson_Test.thy	Wed Jul 08 19:28:43 2015 +0200
@@ -32,7 +32,7 @@
   apply (tactic {* cut_tac xsko25 1 THEN REPEAT (etac exE 1) *})
   ML_val {*
     val ctxt = @{context};
-    val [_, sko25] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal})));
+    val [_, sko25] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
     val clauses25 = Meson.make_clauses ctxt [sko25];   (*7 clauses*)
     val horns25 = Meson.make_horns clauses25;     (*16 Horn clauses*)
     val go25 :: _ = Meson.gocls clauses25;
@@ -56,7 +56,7 @@
   apply (tactic {* cut_tac xsko26 1 THEN REPEAT (etac exE 1) *})
   ML_val {*
     val ctxt = @{context};
-    val [_, sko26] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal})));
+    val [_, sko26] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
     val clauses26 = Meson.make_clauses ctxt [sko26];
     val _ = @{assert} (length clauses26 = 9);
     val horns26 = Meson.make_horns clauses26;
@@ -83,7 +83,7 @@
   apply (tactic {* cut_tac xsko43 1 THEN REPEAT (etac exE 1) *})
   ML_val {*
     val ctxt = @{context};
-    val [_, sko43] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal})));
+    val [_, sko43] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
     val clauses43 = Meson.make_clauses ctxt [sko43];
     val _ = @{assert} (length clauses43 = 6);
     val horns43 = Meson.make_horns clauses43;

--- a/src/Pure/Isar/element.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/Pure/Isar/element.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -215,7 +215,7 @@
 
 fun obtain prop ctxt =
   let
-    val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
+    val ((ps, prop'), ctxt') = Variable.focus NONE prop ctxt;
     fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T, NoSyn);
     val xs = map (fix o #2) ps;
     val As = Logic.strip_imp_prems prop';

--- a/src/Pure/Isar/obtain.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -275,7 +275,7 @@
     val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
     val obtain_rule =
       Thm.forall_elim (Thm.cterm_of ctxt (Logic.varify_global (Free thesis_var))) rule';
-    val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
+    val ((params, stmt), fix_ctxt) = Variable.focus_cterm NONE (Thm.cprem_of obtain_rule 1) ctxt';
     val (prems, ctxt'') =
       Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
         (Drule.strip_imp_prems stmt) fix_ctxt;

--- a/src/Pure/Isar/subgoal.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/Pure/Isar/subgoal.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -15,10 +15,10 @@
   type focus =
    {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
     concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}
-  val focus_params: Proof.context -> int -> thm -> focus * thm
-  val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
-  val focus_prems: Proof.context -> int -> thm -> focus * thm
-  val focus: Proof.context -> int -> thm -> focus * thm
+  val focus_params: Proof.context -> int -> binding list option -> thm -> focus * thm
+  val focus_params_fixed: Proof.context -> int -> binding list option -> thm -> focus * thm
+  val focus_prems: Proof.context -> int -> binding list option -> thm -> focus * thm
+  val focus: Proof.context -> int -> binding list option -> thm -> focus * thm
   val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
     int -> thm -> thm -> thm Seq.seq
   val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
@@ -41,13 +41,13 @@
  {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
   concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list};
 
-fun gen_focus (do_prems, do_concl) ctxt i raw_st =
+fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
   let
     val st = raw_st
       |> Thm.transfer (Proof_Context.theory_of ctxt)
       |> Raw_Simplifier.norm_hhf_protect ctxt;
     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
-    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
+    val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1;
 
     val (asms, concl) =
       if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
@@ -150,7 +150,7 @@
 fun GEN_FOCUS flags tac ctxt i st =
   if Thm.nprems_of st < i then Seq.empty
   else
-    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
+    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i NONE st;
     in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
 
 val FOCUS_PARAMS = GEN_FOCUS (false, false);
@@ -165,10 +165,10 @@
 
 local
 
-fun rename_params ctxt (param_suffix, raw_param_specs) st =
+fun param_bindings ctxt (param_suffix, raw_param_specs) st =
   let
     val _ = if Thm.no_prems st then error "No subgoals!" else ();
-    val (subgoal, goal') = Logic.dest_implies (Thm.prop_of st);
+    val subgoal = #1 (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;
@@ -184,19 +184,16 @@
       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)
+              let
+                val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt));
+                val _ = Variable.check_name b;
+              in SOME 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;
-
-    val subgoal' = rename_prop (rename_list param_specs subgoal_params) subgoal;
-  in Thm.renamed_prop (Logic.mk_implies (subgoal', goal')) st end;
+    fun bindings (SOME x :: xs) (_ :: ys) = x :: bindings xs ys
+      | bindings (NONE :: xs) (y :: ys) = Binding.name y :: bindings xs ys
+      | bindings _ ys = map Binding.name ys;
+  in bindings param_specs subgoal_params end;
 
 fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
   let
@@ -212,8 +209,8 @@
       | NONE => ((Binding.empty, []), false));
 
     val (subgoal_focus, _) =
-      rename_params ctxt param_specs st
-      |> (if do_prems then focus else focus_params_fixed) ctxt 1;
+      (if do_prems then focus else focus_params_fixed) ctxt
+        1 (SOME (param_bindings ctxt param_specs st)) st;
 
     fun after_qed (ctxt'', [[result]]) =
       Proof.end_block #> (fn state' =>

--- a/src/Pure/Tools/rule_insts.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -218,7 +218,7 @@
     val ((_, params), ctxt') = ctxt
       |> Variable.declare_constraints goal
       |> Variable.improper_fixes
-      |> Variable.focus_params goal
+      |> Variable.focus_params NONE goal
       ||> Variable.restore_proper_fixes ctxt;
   in (params, ctxt') end;
 

--- a/src/Pure/goal.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/Pure/goal.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -328,7 +328,7 @@
 
 fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
   let
-    val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
+    val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt;
     val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
     val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
     val tacs = Rs |> map (fn R =>

--- a/src/Pure/variable.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/Pure/variable.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -78,10 +78,14 @@
     ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context
   val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
   val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
-  val focus_params: term -> Proof.context -> (string list * (string * typ) list) * Proof.context
-  val focus: term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context
-  val focus_cterm: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
-  val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
+  val focus_params: binding list option -> term -> Proof.context ->
+    (string list * (string * typ) list) * Proof.context
+  val focus: binding list option -> term -> Proof.context ->
+    ((string * (string * typ)) list * term) * Proof.context
+  val focus_cterm: binding list option -> cterm -> Proof.context ->
+    ((string * cterm) list * cterm) * Proof.context
+  val focus_subgoal: binding list option -> int -> thm -> Proof.context ->
+    ((string * cterm) list * cterm) * Proof.context
   val warn_extra_tfrees: Proof.context -> Proof.context -> unit
   val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
   val polymorphic: Proof.context -> term list -> term list
@@ -616,18 +620,21 @@
 
 (* focus on outermost parameters: !!x y z. B *)
 
-fun focus_params t ctxt =
+fun focus_params bindings t ctxt =
   let
     val (xs, Ts) =
       split_list (Term.variant_frees t (Term.strip_all_vars t));  (*as they are printed :-*)
-    val (xs', ctxt') = variant_fixes xs ctxt;
+    val (xs', ctxt') =
+      (case bindings of
+        SOME bs => ctxt |> set_body true |> add_fixes_binding bs ||> restore_body ctxt
+      | NONE => ctxt |> variant_fixes xs);
     val ps = xs' ~~ Ts;
     val ctxt'' = ctxt' |> fold (declare_constraints o Free) ps;
   in ((xs, ps), ctxt'') end;
 
-fun focus t ctxt =
+fun focus bindings t ctxt =
   let
-    val ((xs, ps), ctxt') = focus_params t ctxt;
+    val ((xs, ps), ctxt') = focus_params bindings t ctxt;
     val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t);
   in (((xs ~~ ps), t'), ctxt') end;
 
@@ -635,20 +642,20 @@
   Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t)
   |> Thm.cprop_of |> Thm.dest_arg;
 
-fun focus_cterm goal ctxt =
+fun focus_cterm bindings goal ctxt =
   let
-    val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt;
+    val ((xs, ps), ctxt') = focus_params bindings (Thm.term_of goal) ctxt;
     val ps' = map (Thm.cterm_of ctxt' o Free) ps;
     val goal' = fold forall_elim_prop ps' goal;
   in ((xs ~~ ps', goal'), ctxt') end;
 
-fun focus_subgoal i st =
+fun focus_subgoal bindings i st =
   let
     val all_vars = Thm.fold_terms Term.add_vars st [];
   in
     fold (unbind_term o #1) all_vars #>
     fold (declare_constraints o Var) all_vars #>
-    focus_cterm (Thm.cprem_of st i)
+    focus_cterm bindings (Thm.cprem_of st i)
   end;
 
 

--- a/src/Tools/induct_tacs.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/Tools/induct_tacs.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -68,7 +68,7 @@
   let
     val goal = Thm.cprem_of st i;
     val (_, goal_ctxt) = Rule_Insts.goal_context (Thm.term_of goal) ctxt
-    and ((_, goal'), _) = Variable.focus_cterm goal ctxt;
+    and ((_, goal'), _) = Variable.focus_cterm NONE goal ctxt;
     val (prems, concl) = Logic.strip_horn (Thm.term_of goal');
 
     fun induct_var name =

--- a/src/ZF/Tools/induct_tacs.ML	Wed Jul 08 15:37:32 2015 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Wed Jul 08 19:28:43 2015 +0200
@@ -93,7 +93,7 @@
 fun exhaust_induct_tac exh ctxt var fixes i state = SUBGOAL (fn _ =>
   let
     val thy = Proof_Context.theory_of ctxt
-    val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
+    val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i NONE state
     val tn = find_tname ctxt' var (map Thm.term_of asms)
     val rule =
         if exh then #exhaustion (datatype_info thy tn)