activate Defines: fix frees;

--- a/src/Pure/Isar/locale.ML	Fri May 26 22:20:05 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Fri May 26 22:20:06 2006 +0200
@@ -860,11 +860,12 @@
   | activate_elem _ ((ctxt, Assumed axs), Defines defs) =
       let
         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 |> ProofContext.add_assms_i LocalDefs.def_export
-          (defs' |> map (fn ((name, atts), (t, ps)) =>
-            let val ((c, _), t') = LocalDefs.cert_def ctxt t
-            in ((if name = "" then Thm.def_name c else name, atts), [(t', ps)]) end))
+          ctxt |> fold (ProofContext.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), [])