src/Pure/variable.ML

 fun revert_bounds ctxt t =
   (case #2 (#bounds (rep_data ctxt)) of
     [] => t
   | bounds =>
       let
-        val names = Term.declare_term_names t (names_of ctxt);
+        val names = Term.declare_free_names t (names_of ctxt);
         val xs = rev (Name.variants names (rev (map #2 bounds)));
         fun substs (((b, T), _), x') =
           let fun subst U = (Free (b, U), Syntax_Trans.mark_bound_abs (x', U))
           in [subst T, subst (Type_Annotation.ignore_type T)] end;
       in Term.subst_atomic (maps substs (bounds ~~ xs)) t end);

 val set_bound_focus = Config.put bound_focus;
 val restore_bound_focus = set_bound_focus o is_bound_focus;
 
 fun focus_params bindings t ctxt =
   let
-    val ps = Term.variant_frees t (Term.strip_all_vars t);  (*as they are printed :-*)
+    val ps = Term.variant_bounds t (Term.strip_all_vars t);
     val (xs, Ts) = split_list ps;
     val (xs', ctxt') =
       (case bindings of
         SOME bs => ctxt |> set_body true |> add_fixes_binding bs ||> restore_body ctxt
       | NONE => if is_bound_focus ctxt then bound_fixes ps ctxt else variant_fixes xs ctxt);