--- 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), [])