prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;

--- 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 *)

--- 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