# HG changeset patch # User wenzelm # Date 1427560002 -3600 # Node ID 0e9baaf0e0bb5ede23b8455525ee2de8aa60490f # Parent 04e569577c18884374ec998402dbdbf88aa62dc5 prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars; diff -r 04e569577c18 -r 0e9baaf0e0bb src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Fri Mar 27 19:51:05 2015 +0100 +++ b/src/Pure/Tools/rule_insts.ML Sat Mar 28 17:26:42 2015 +0100 @@ -214,19 +214,13 @@ fun goal_context i st ctxt = let val goal = Thm.term_of (Thm.cprem_of st i); - val params = - Logic.strip_params goal - (*as they are printed: bound variables with the same name are renamed*) - |> Term.rename_wrt_term goal - |> rev; - val (param_names, param_ctxt) = ctxt + val ((_, params), ctxt') = ctxt |> Thm.fold_terms Variable.declare_constraints st |> Variable.improper_fixes - |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params) + |> Variable.focus_params goal ||> Variable.restore_proper_fixes ctxt ||> Config.get ctxt schematic ? Proof_Context.set_mode Proof_Context.mode_schematic; - val paramTs = map #2 params; - in (param_names ~~ paramTs, param_ctxt) end; + in (params, ctxt') end; (* resolution after lifting and instantiation; may refer to parameters of the subgoal *) diff -r 04e569577c18 -r 0e9baaf0e0bb src/Pure/variable.ML --- a/src/Pure/variable.ML Fri Mar 27 19:51:05 2015 +0100 +++ b/src/Pure/variable.ML Sat Mar 28 17:26:42 2015 +0100 @@ -73,6 +73,7 @@ (((ctyp * ctyp) list * (cterm * 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