diff -r cfea8e7f9ebd -r 8b64a1ea9b1b src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Jul 27 23:28:27 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Jul 27 23:28:28 2006 +0200
@@ -882,7 +882,7 @@
         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) =
@@ -894,7 +894,7 @@
             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) =