src/Pure/Isar/locale.ML

       let
         val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
         val ts = maps (map #1 o #2) asms';
         val (ps, qs) = chop (length ts) axs;
         val (_, ctxt') =
-          ctxt |> fold ProofContext.fix_frees ts
+          ctxt |> fold Variable.fix_frees ts
           |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
       in ((ctxt', Assumed qs), []) end
   | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
       ((ctxt, Derived ths), [])
   | activate_elem _ _ ((ctxt, Assumed axs), Defines defs) =

         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = LocalDefs.cert_def ctxt t
             in (t', ((if name = "" then Thm.def_name c else name, atts), [(t', ps)])) end);
         val (_, ctxt') =
-          ctxt |> fold (ProofContext.fix_frees o #1) asms
+          ctxt |> fold (Variable.fix_frees o #1) asms
           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
       in ((ctxt', Assumed axs), []) end
   | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
       ((ctxt, Derived ths), [])
   | activate_elem _ is_ext ((ctxt, mode), Notes facts) =