Variable.focus etc.: optional bindings provided by user;
authorwenzelm
Wed Jul 08 19:28:43 2015 +0200 (2015-07-08)
changeset 60695757549b4bbe6
parent 60694 b3fa4a8cdb5f
child 60696 8304fb4fb823
Variable.focus etc.: optional bindings provided by user;
Subgoal.focus command: more careful treatment of user-provided bindings;
src/Doc/Implementation/Proof.thy
src/HOL/Eisbach/match_method.ML
src/HOL/Library/Old_SMT/old_smt_solver.ML
src/HOL/Tools/Function/function_context_tree.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/ex/Meson_Test.thy
src/Pure/Isar/element.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/subgoal.ML
src/Pure/Tools/rule_insts.ML
src/Pure/goal.ML
src/Pure/variable.ML
src/Tools/induct_tacs.ML
src/ZF/Tools/induct_tacs.ML
     1.1 --- a/src/Doc/Implementation/Proof.thy	Wed Jul 08 15:37:32 2015 +0200
     1.2 +++ b/src/Doc/Implementation/Proof.thy	Wed Jul 08 19:28:43 2015 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4    @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
     1.5    @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
     1.6    ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context"} \\
     1.7 -  @{index_ML Variable.focus: "term -> Proof.context ->
     1.8 +  @{index_ML Variable.focus: "binding list option -> term -> Proof.context ->
     1.9    ((string * (string * typ)) list * term) * Proof.context"} \\
    1.10    \end{mldecls}
    1.11  
    1.12 @@ -153,8 +153,8 @@
    1.13    should be accessible to the user, otherwise newly introduced names
    1.14    are marked as ``internal'' (\secref{sec:names}).
    1.15  
    1.16 -  \item @{ML Variable.focus}~@{text B} decomposes the outermost @{text
    1.17 -  "\<And>"} prefix of proposition @{text "B"}.
    1.18 +  \item @{ML Variable.focus}~@{text "bindings B"} decomposes the outermost @{text
    1.19 +  "\<And>"} prefix of proposition @{text "B"}, using the given name bindings.
    1.20  
    1.21    \end{description}
    1.22  \<close>
    1.23 @@ -394,9 +394,12 @@
    1.24    Proof.context -> int -> tactic"} \\
    1.25    @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) ->
    1.26    Proof.context -> int -> tactic"} \\
    1.27 -  @{index_ML Subgoal.focus: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
    1.28 -  @{index_ML Subgoal.focus_prems: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
    1.29 -  @{index_ML Subgoal.focus_params: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
    1.30 +  @{index_ML Subgoal.focus: "Proof.context -> int -> binding list option ->
    1.31 +  thm -> Subgoal.focus * thm"} \\
    1.32 +  @{index_ML Subgoal.focus_prems: "Proof.context -> int -> binding list option ->
    1.33 +  thm -> Subgoal.focus * thm"} \\
    1.34 +  @{index_ML Subgoal.focus_params: "Proof.context -> int -> binding list option ->
    1.35 +  thm -> Subgoal.focus * thm"} \\
    1.36    \end{mldecls}
    1.37  
    1.38    \begin{mldecls}
    1.39 @@ -473,7 +476,7 @@
    1.40      ML_val
    1.41       \<open>val {goal, context = goal_ctxt, ...} = @{Isar.goal};
    1.42        val (focus as {params, asms, concl, ...}, goal') =
    1.43 -        Subgoal.focus goal_ctxt 1 goal;
    1.44 +        Subgoal.focus goal_ctxt 1 (SOME [@{binding x}]) goal;
    1.45        val [A, B] = #prems focus;
    1.46        val [(_, x)] = #params focus;\<close>
    1.47      sorry
     2.1 --- a/src/HOL/Eisbach/match_method.ML	Wed Jul 08 15:37:32 2015 +0200
     2.2 +++ b/src/HOL/Eisbach/match_method.ML	Wed Jul 08 19:28:43 2015 +0200
     2.3 @@ -304,7 +304,7 @@
     2.4  
     2.5  fun prep_fact_pat ((x, args), pat) ctxt =
     2.6    let
     2.7 -    val ((params, pat'), ctxt') = Variable.focus pat ctxt;
     2.8 +    val ((params, pat'), ctxt') = Variable.focus NONE pat ctxt;
     2.9      val params' = map (Free o snd) params;
    2.10  
    2.11      val morphism =
    2.12 @@ -500,10 +500,10 @@
    2.13  
    2.14  
    2.15  (* Fix schematics in the goal *)
    2.16 -fun focus_concl ctxt i goal =
    2.17 +fun focus_concl ctxt i bindings goal =
    2.18    let
    2.19      val ({context = ctxt', concl, params, prems, asms, schematics}, goal') =
    2.20 -      Subgoal.focus_params ctxt i goal;
    2.21 +      Subgoal.focus_params ctxt i bindings goal;
    2.22  
    2.23      val (inst, ctxt'') = Variable.import_inst true [Thm.term_of concl] ctxt';
    2.24      val (_, schematic_terms) = Thm.certify_inst ctxt'' inst;
    2.25 @@ -711,7 +711,7 @@
    2.26              val (goal_thins, goal) = get_thinned_prems goal;
    2.27  
    2.28              val ((local_premids, {context = focus_ctxt, params, asms, concl, ...}), focused_goal) =
    2.29 -              focus_cases (K Subgoal.focus_prems) (focus_concl) ctxt 1 goal
    2.30 +              focus_cases (K Subgoal.focus_prems) focus_concl ctxt 1 NONE goal
    2.31                |>> augment_focus;
    2.32  
    2.33              val texts =
     3.1 --- a/src/HOL/Library/Old_SMT/old_smt_solver.ML	Wed Jul 08 15:37:32 2015 +0200
     3.2 +++ b/src/HOL/Library/Old_SMT/old_smt_solver.ML	Wed Jul 08 19:28:43 2015 +0200
     3.3 @@ -281,7 +281,7 @@
     3.4        |> Config.put Old_SMT_Config.oracle false
     3.5        |> Config.put Old_SMT_Config.filter_only_facts true
     3.6  
     3.7 -    val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
     3.8 +    val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i NONE goal
     3.9      fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply
    3.10      val cprop =
    3.11        (case try negate (Thm.rhs_of (Old_SMT_Normalize.atomize_conv ctxt' concl)) of
     4.1 --- a/src/HOL/Tools/Function/function_context_tree.ML	Wed Jul 08 15:37:32 2015 +0200
     4.2 +++ b/src/HOL/Tools/Function/function_context_tree.ML	Wed Jul 08 19:28:43 2015 +0200
     4.3 @@ -103,7 +103,7 @@
     4.4  (* Called on the INSTANTIATED branches of the congruence rule *)
     4.5  fun mk_branch ctxt t =
     4.6    let
     4.7 -    val ((params, impl), ctxt') = Variable.focus t ctxt
     4.8 +    val ((params, impl), ctxt') = Variable.focus NONE t ctxt
     4.9      val (assms, concl) = Logic.strip_horn impl
    4.10    in
    4.11      (ctxt', map #2 params, assms, rhs_of concl)
     5.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Wed Jul 08 15:37:32 2015 +0200
     5.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Jul 08 19:28:43 2015 +0200
     5.3 @@ -53,7 +53,7 @@
     5.4  
     5.5  fun dest_hhf ctxt t =
     5.6    let
     5.7 -    val ((params, imp), ctxt') = Variable.focus t ctxt
     5.8 +    val ((params, imp), ctxt') = Variable.focus NONE t ctxt
     5.9    in
    5.10      (ctxt', map #2 params, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp)
    5.11    end
     6.1 --- a/src/HOL/Tools/Function/partial_function.ML	Wed Jul 08 15:37:32 2015 +0200
     6.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Wed Jul 08 19:28:43 2015 +0200
     6.3 @@ -230,7 +230,7 @@
     6.4      val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data;
     6.5  
     6.6      val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
     6.7 -    val ((_, plain_eqn), args_ctxt) = Variable.focus eqn lthy;
     6.8 +    val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy;
     6.9  
    6.10      val ((f_binding, fT), mixfix) = the_single fixes;
    6.11      val fname = Binding.name_of f_binding;
     7.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Jul 08 15:37:32 2015 +0200
     7.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Jul 08 19:28:43 2015 +0200
     7.3 @@ -252,7 +252,7 @@
     7.4    let
     7.5      val ctxt = ctxt0 |> Config.put SMT_Config.timeout (Time.toReal time_limit)
     7.6  
     7.7 -    val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i goal
     7.8 +    val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i NONE goal
     7.9      fun negate ct = Thm.dest_comb ct ||> Thm.apply @{cterm Not} |-> Thm.apply
    7.10      val cprop =
    7.11        (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt concl)) of
     8.1 --- a/src/HOL/ex/Meson_Test.thy	Wed Jul 08 15:37:32 2015 +0200
     8.2 +++ b/src/HOL/ex/Meson_Test.thy	Wed Jul 08 19:28:43 2015 +0200
     8.3 @@ -32,7 +32,7 @@
     8.4    apply (tactic {* cut_tac xsko25 1 THEN REPEAT (etac exE 1) *})
     8.5    ML_val {*
     8.6      val ctxt = @{context};
     8.7 -    val [_, sko25] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal})));
     8.8 +    val [_, sko25] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
     8.9      val clauses25 = Meson.make_clauses ctxt [sko25];   (*7 clauses*)
    8.10      val horns25 = Meson.make_horns clauses25;     (*16 Horn clauses*)
    8.11      val go25 :: _ = Meson.gocls clauses25;
    8.12 @@ -56,7 +56,7 @@
    8.13    apply (tactic {* cut_tac xsko26 1 THEN REPEAT (etac exE 1) *})
    8.14    ML_val {*
    8.15      val ctxt = @{context};
    8.16 -    val [_, sko26] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal})));
    8.17 +    val [_, sko26] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
    8.18      val clauses26 = Meson.make_clauses ctxt [sko26];
    8.19      val _ = @{assert} (length clauses26 = 9);
    8.20      val horns26 = Meson.make_horns clauses26;
    8.21 @@ -83,7 +83,7 @@
    8.22    apply (tactic {* cut_tac xsko43 1 THEN REPEAT (etac exE 1) *})
    8.23    ML_val {*
    8.24      val ctxt = @{context};
    8.25 -    val [_, sko43] = #prems (#1 (Subgoal.focus ctxt 1 (#goal @{Isar.goal})));
    8.26 +    val [_, sko43] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
    8.27      val clauses43 = Meson.make_clauses ctxt [sko43];
    8.28      val _ = @{assert} (length clauses43 = 6);
    8.29      val horns43 = Meson.make_horns clauses43;
     9.1 --- a/src/Pure/Isar/element.ML	Wed Jul 08 15:37:32 2015 +0200
     9.2 +++ b/src/Pure/Isar/element.ML	Wed Jul 08 19:28:43 2015 +0200
     9.3 @@ -215,7 +215,7 @@
     9.4  
     9.5  fun obtain prop ctxt =
     9.6    let
     9.7 -    val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
     9.8 +    val ((ps, prop'), ctxt') = Variable.focus NONE prop ctxt;
     9.9      fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T, NoSyn);
    9.10      val xs = map (fix o #2) ps;
    9.11      val As = Logic.strip_imp_prems prop';
    10.1 --- a/src/Pure/Isar/obtain.ML	Wed Jul 08 15:37:32 2015 +0200
    10.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jul 08 19:28:43 2015 +0200
    10.3 @@ -275,7 +275,7 @@
    10.4      val ((_, [rule']), ctxt') = Variable.import false [closed_rule] ctxt;
    10.5      val obtain_rule =
    10.6        Thm.forall_elim (Thm.cterm_of ctxt (Logic.varify_global (Free thesis_var))) rule';
    10.7 -    val ((params, stmt), fix_ctxt) = Variable.focus_cterm (Thm.cprem_of obtain_rule 1) ctxt';
    10.8 +    val ((params, stmt), fix_ctxt) = Variable.focus_cterm NONE (Thm.cprem_of obtain_rule 1) ctxt';
    10.9      val (prems, ctxt'') =
   10.10        Assumption.add_assms (obtain_export fix_ctxt obtain_rule (map #2 params))
   10.11          (Drule.strip_imp_prems stmt) fix_ctxt;
    11.1 --- a/src/Pure/Isar/subgoal.ML	Wed Jul 08 15:37:32 2015 +0200
    11.2 +++ b/src/Pure/Isar/subgoal.ML	Wed Jul 08 19:28:43 2015 +0200
    11.3 @@ -15,10 +15,10 @@
    11.4    type focus =
    11.5     {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
    11.6      concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list}
    11.7 -  val focus_params: Proof.context -> int -> thm -> focus * thm
    11.8 -  val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
    11.9 -  val focus_prems: Proof.context -> int -> thm -> focus * thm
   11.10 -  val focus: Proof.context -> int -> thm -> focus * thm
   11.11 +  val focus_params: Proof.context -> int -> binding list option -> thm -> focus * thm
   11.12 +  val focus_params_fixed: Proof.context -> int -> binding list option -> thm -> focus * thm
   11.13 +  val focus_prems: Proof.context -> int -> binding list option -> thm -> focus * thm
   11.14 +  val focus: Proof.context -> int -> binding list option -> thm -> focus * thm
   11.15    val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
   11.16      int -> thm -> thm -> thm Seq.seq
   11.17    val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
   11.18 @@ -41,13 +41,13 @@
   11.19   {context: Proof.context, params: (string * cterm) list, prems: thm list, asms: cterm list,
   11.20    concl: cterm, schematics: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list};
   11.21  
   11.22 -fun gen_focus (do_prems, do_concl) ctxt i raw_st =
   11.23 +fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
   11.24    let
   11.25      val st = raw_st
   11.26        |> Thm.transfer (Proof_Context.theory_of ctxt)
   11.27        |> Raw_Simplifier.norm_hhf_protect ctxt;
   11.28      val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
   11.29 -    val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
   11.30 +    val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1;
   11.31  
   11.32      val (asms, concl) =
   11.33        if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
   11.34 @@ -150,7 +150,7 @@
   11.35  fun GEN_FOCUS flags tac ctxt i st =
   11.36    if Thm.nprems_of st < i then Seq.empty
   11.37    else
   11.38 -    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
   11.39 +    let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i NONE st;
   11.40      in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
   11.41  
   11.42  val FOCUS_PARAMS = GEN_FOCUS (false, false);
   11.43 @@ -165,10 +165,10 @@
   11.44  
   11.45  local
   11.46  
   11.47 -fun rename_params ctxt (param_suffix, raw_param_specs) st =
   11.48 +fun param_bindings ctxt (param_suffix, raw_param_specs) st =
   11.49    let
   11.50      val _ = if Thm.no_prems st then error "No subgoals!" else ();
   11.51 -    val (subgoal, goal') = Logic.dest_implies (Thm.prop_of st);
   11.52 +    val subgoal = #1 (Logic.dest_implies (Thm.prop_of st));
   11.53      val subgoal_params =
   11.54        map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
   11.55        |> Term.variant_frees subgoal |> map #1;
   11.56 @@ -184,19 +184,16 @@
   11.57        raw_param_specs |> map
   11.58          (fn (NONE, _) => NONE
   11.59            | (SOME x, pos) =>
   11.60 -              let val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
   11.61 -              in SOME (Variable.check_name b) end)
   11.62 +              let
   11.63 +                val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt));
   11.64 +                val _ = Variable.check_name b;
   11.65 +              in SOME b end)
   11.66        |> param_suffix ? append (replicate (n - m) NONE);
   11.67  
   11.68 -    fun rename_list (opt_x :: xs) (y :: ys) = (the_default y opt_x :: rename_list xs ys)
   11.69 -      | rename_list _ ys = ys;
   11.70 -
   11.71 -    fun rename_prop (x :: xs) ((c as Const ("Pure.all", _)) $ Abs (_, T, t)) =
   11.72 -          (c $ Abs (x, T, rename_prop xs t))
   11.73 -      | rename_prop [] t = t;
   11.74 -
   11.75 -    val subgoal' = rename_prop (rename_list param_specs subgoal_params) subgoal;
   11.76 -  in Thm.renamed_prop (Logic.mk_implies (subgoal', goal')) st end;
   11.77 +    fun bindings (SOME x :: xs) (_ :: ys) = x :: bindings xs ys
   11.78 +      | bindings (NONE :: xs) (y :: ys) = Binding.name y :: bindings xs ys
   11.79 +      | bindings _ ys = map Binding.name ys;
   11.80 +  in bindings param_specs subgoal_params end;
   11.81  
   11.82  fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
   11.83    let
   11.84 @@ -212,8 +209,8 @@
   11.85        | NONE => ((Binding.empty, []), false));
   11.86  
   11.87      val (subgoal_focus, _) =
   11.88 -      rename_params ctxt param_specs st
   11.89 -      |> (if do_prems then focus else focus_params_fixed) ctxt 1;
   11.90 +      (if do_prems then focus else focus_params_fixed) ctxt
   11.91 +        1 (SOME (param_bindings ctxt param_specs st)) st;
   11.92  
   11.93      fun after_qed (ctxt'', [[result]]) =
   11.94        Proof.end_block #> (fn state' =>
    12.1 --- a/src/Pure/Tools/rule_insts.ML	Wed Jul 08 15:37:32 2015 +0200
    12.2 +++ b/src/Pure/Tools/rule_insts.ML	Wed Jul 08 19:28:43 2015 +0200
    12.3 @@ -218,7 +218,7 @@
    12.4      val ((_, params), ctxt') = ctxt
    12.5        |> Variable.declare_constraints goal
    12.6        |> Variable.improper_fixes
    12.7 -      |> Variable.focus_params goal
    12.8 +      |> Variable.focus_params NONE goal
    12.9        ||> Variable.restore_proper_fixes ctxt;
   12.10    in (params, ctxt') end;
   12.11  
    13.1 --- a/src/Pure/goal.ML	Wed Jul 08 15:37:32 2015 +0200
    13.2 +++ b/src/Pure/goal.ML	Wed Jul 08 19:28:43 2015 +0200
    13.3 @@ -328,7 +328,7 @@
    13.4  
    13.5  fun assume_rule_tac ctxt = norm_hhf_tac ctxt THEN' CSUBGOAL (fn (goal, i) =>
    13.6    let
    13.7 -    val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
    13.8 +    val ((_, goal'), ctxt') = Variable.focus_cterm NONE goal ctxt;
    13.9      val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
   13.10      val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
   13.11      val tacs = Rs |> map (fn R =>
    14.1 --- a/src/Pure/variable.ML	Wed Jul 08 15:37:32 2015 +0200
    14.2 +++ b/src/Pure/variable.ML	Wed Jul 08 19:28:43 2015 +0200
    14.3 @@ -78,10 +78,14 @@
    14.4      ((((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list) * thm list) * Proof.context
    14.5    val tradeT: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
    14.6    val trade: (Proof.context -> thm list -> thm list) -> Proof.context -> thm list -> thm list
    14.7 -  val focus_params: term -> Proof.context -> (string list * (string * typ) list) * Proof.context
    14.8 -  val focus: term -> Proof.context -> ((string * (string * typ)) list * term) * Proof.context
    14.9 -  val focus_cterm: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
   14.10 -  val focus_subgoal: int -> thm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context
   14.11 +  val focus_params: binding list option -> term -> Proof.context ->
   14.12 +    (string list * (string * typ) list) * Proof.context
   14.13 +  val focus: binding list option -> term -> Proof.context ->
   14.14 +    ((string * (string * typ)) list * term) * Proof.context
   14.15 +  val focus_cterm: binding list option -> cterm -> Proof.context ->
   14.16 +    ((string * cterm) list * cterm) * Proof.context
   14.17 +  val focus_subgoal: binding list option -> int -> thm -> Proof.context ->
   14.18 +    ((string * cterm) list * cterm) * Proof.context
   14.19    val warn_extra_tfrees: Proof.context -> Proof.context -> unit
   14.20    val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
   14.21    val polymorphic: Proof.context -> term list -> term list
   14.22 @@ -616,18 +620,21 @@
   14.23  
   14.24  (* focus on outermost parameters: !!x y z. B *)
   14.25  
   14.26 -fun focus_params t ctxt =
   14.27 +fun focus_params bindings t ctxt =
   14.28    let
   14.29      val (xs, Ts) =
   14.30        split_list (Term.variant_frees t (Term.strip_all_vars t));  (*as they are printed :-*)
   14.31 -    val (xs', ctxt') = variant_fixes xs ctxt;
   14.32 +    val (xs', ctxt') =
   14.33 +      (case bindings of
   14.34 +        SOME bs => ctxt |> set_body true |> add_fixes_binding bs ||> restore_body ctxt
   14.35 +      | NONE => ctxt |> variant_fixes xs);
   14.36      val ps = xs' ~~ Ts;
   14.37      val ctxt'' = ctxt' |> fold (declare_constraints o Free) ps;
   14.38    in ((xs, ps), ctxt'') end;
   14.39  
   14.40 -fun focus t ctxt =
   14.41 +fun focus bindings t ctxt =
   14.42    let
   14.43 -    val ((xs, ps), ctxt') = focus_params t ctxt;
   14.44 +    val ((xs, ps), ctxt') = focus_params bindings t ctxt;
   14.45      val t' = Term.subst_bounds (rev (map Free ps), Term.strip_all_body t);
   14.46    in (((xs ~~ ps), t'), ctxt') end;
   14.47  
   14.48 @@ -635,20 +642,20 @@
   14.49    Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t)
   14.50    |> Thm.cprop_of |> Thm.dest_arg;
   14.51  
   14.52 -fun focus_cterm goal ctxt =
   14.53 +fun focus_cterm bindings goal ctxt =
   14.54    let
   14.55 -    val ((xs, ps), ctxt') = focus_params (Thm.term_of goal) ctxt;
   14.56 +    val ((xs, ps), ctxt') = focus_params bindings (Thm.term_of goal) ctxt;
   14.57      val ps' = map (Thm.cterm_of ctxt' o Free) ps;
   14.58      val goal' = fold forall_elim_prop ps' goal;
   14.59    in ((xs ~~ ps', goal'), ctxt') end;
   14.60  
   14.61 -fun focus_subgoal i st =
   14.62 +fun focus_subgoal bindings i st =
   14.63    let
   14.64      val all_vars = Thm.fold_terms Term.add_vars st [];
   14.65    in
   14.66      fold (unbind_term o #1) all_vars #>
   14.67      fold (declare_constraints o Var) all_vars #>
   14.68 -    focus_cterm (Thm.cprem_of st i)
   14.69 +    focus_cterm bindings (Thm.cprem_of st i)
   14.70    end;
   14.71  
   14.72  
    15.1 --- a/src/Tools/induct_tacs.ML	Wed Jul 08 15:37:32 2015 +0200
    15.2 +++ b/src/Tools/induct_tacs.ML	Wed Jul 08 19:28:43 2015 +0200
    15.3 @@ -68,7 +68,7 @@
    15.4    let
    15.5      val goal = Thm.cprem_of st i;
    15.6      val (_, goal_ctxt) = Rule_Insts.goal_context (Thm.term_of goal) ctxt
    15.7 -    and ((_, goal'), _) = Variable.focus_cterm goal ctxt;
    15.8 +    and ((_, goal'), _) = Variable.focus_cterm NONE goal ctxt;
    15.9      val (prems, concl) = Logic.strip_horn (Thm.term_of goal');
   15.10  
   15.11      fun induct_var name =
    16.1 --- a/src/ZF/Tools/induct_tacs.ML	Wed Jul 08 15:37:32 2015 +0200
    16.2 +++ b/src/ZF/Tools/induct_tacs.ML	Wed Jul 08 19:28:43 2015 +0200
    16.3 @@ -93,7 +93,7 @@
    16.4  fun exhaust_induct_tac exh ctxt var fixes i state = SUBGOAL (fn _ =>
    16.5    let
    16.6      val thy = Proof_Context.theory_of ctxt
    16.7 -    val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
    16.8 +    val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i NONE state
    16.9      val tn = find_tname ctxt' var (map Thm.term_of asms)
   16.10      val rule =
   16.11          if exh then #exhaustion (datatype_info thy tn)